proposition: Lemma C_RInt_segm_correct (f : C -> C) (z1 z2 : C) : ex_C_RInt_segm f z1 z2 -> is_C_RInt_segm f z1 z2 (C_RInt_segm f z1 z2).
proof: Proof. intros [l If]. now rewrite (is_C_RInt_segm_unique _ _ _ _ If). Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)