proposition: Lemma ex_C_RInt_segm_swap (f : C -> C) (z1 z2 : C) : ex_C_RInt_segm f z2 z1 -> ex_C_RInt_segm f z1 z2.
proof: Proof. intros [l Hl]. exists (-l) ; by apply is_C_RInt_segm_swap. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)