On décompose : 
- le trajet A-K-B  en AI + IK + KB 
- le trajer A-C-B en AC + CO + OB.

On montre que chaque morceau du 
premier trajet est lus long (en temps)
que son homologue du deuxième.

i1 = 0.5235987755982991 rad (slider from 0 to 6.283185307179586, step 0.017453292519943295)
C = Intersect(a, b)
E = Point(b)
F = Point(b)
i = (0, 1)
A = Rotate(E, i1, C)
i_1 = Angle(E, C, A)
c = Ray(C, A)
v_1 = 2
v_2 = 2.7
i2: asin(v_2 / v_1 * sin(i1)) * 180.0 / 3.141592653589793
B = Rotate(F, i2°, C)
i_2 = Angle(F, C, B)
d = Ray(C, B)
K = Point(a)
K' = Rotate(K, i1, C)
α = Angle(K, C, K')
e = Ray(C, K')
f = OrthogonalLine(K, e)
H = Intersect(f, e)
poly1, b_1, a_1, k = Polygon(C, K, H)
g = OrthogonalLine(K, d)
O = Intersect(g, d)
poly2, k_1, a_2, o = Polygon(C, O, K)
β = Angle(C, K, O)
γ = Angle(C, H, K)
δ = Angle(K, O, C)
h = Segment(A, K)
j = Segment(K, B)
I = Intersect(h, e)