proposition: Lemma complex_segment_triangle (a b c : C) (z : C) : complex_segment b c z -> complex_triangle a b c z.
proof: Proof. intros (p,(Hp,->)). exists 0,(1-p)%R,p. repeat split => //. by apply Rle_refl. apply -> Rminus_le_0 ; apply Hp. by apply Hp. ring. rewrite !scal_R_Cmult !RtoC_minus. by ring_simplify. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)