proposition: Lemma 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 -> C_RInt_segm f z1 z2 + C_RInt_segm f z2 z3 = C_RInt_segm f z1 z3.
proof: Proof. intros. apply sym_eq, is_C_RInt_segm_unique. now apply is_C_RInt_segm_Chasles with z2 ; try (by apply C_RInt_segm_correct). Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)