proposition: Lemma complex_segment_Chasles (z1 z2 z3 : C) : complex_segment z1 z3 z2 -> forall (z : C), complex_segment z1 z2 z -> complex_segment z1 z3 z.
proof: Proof. intros [p2 [Hp2 ->]] _ [p [Hp ->]]. exists (p * p2)%R ; repeat split. apply Rmult_le_pos, Hp2 ; apply Hp. rewrite -(Rmult_1_r 1). apply Rmult_le_compat ; intuition. rewrite !scal_R_Cmult !RtoC_minus RtoC_mult ; ring. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)