proposition: Lemma complex_segment_swap z1 z2 : forall z, complex_segment z1 z2 z -> complex_segment z2 z1 z.
proof: Proof. move => _ [z [Hz ->]]. exists (1 - z)%R ; split. split. apply Rle_minus_r ; ring_simplify ; apply Hz. apply Rminus_le_0 ; ring_simplify ; apply Hz. rewrite !scal_R_Cmult !RtoC_minus ; ring. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)