proposition: Lemma ex_C_RInt_segm_Chasles (f : C -> C) (z1 z2 z3 : C) : complex_line z1 z3 z2 -> ex_C_RInt_segm f z1 z2 -> ex_C_RInt_segm f z2 z3 -> ex_C_RInt_segm f z1 z3.
proof: Proof. intros Hz2 [l1 H1] [l2 H2] ; exists (plus l1 l2) ; by apply is_C_RInt_segm_Chasles with z2. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)