proposition: Lemma complex_triangle_diameter_segment (a b c : C) : forall z, complex_segment b c z -> Cmod (z - a) <= complex_triangle_diameter a b c.
proof: Proof. intros _ (p,(Hp,->)). rewrite !scal_R_Cmult RtoC_minus. replace ((1 - p) * b + p * c - a) with ((1 - p) * (b - a) + p * (c - a)) by ring. eapply Rle_trans. apply Cmod_triangle. rewrite !Cmod_mult -RtoC_minus !Cmod_R. eapply Rle_trans. apply Rplus_le_compat ; apply Rmult_le_compat_l ; try apply Rabs_pos. apply (Rmax_l _ (Cmod (c - a))). apply (Rmax_r (Cmod (b - a))). rewrite -Rmult_plus_distr_r. rewrite !Rabs_pos_eq. ring_simplify ; rewrite /complex_triangle_diameter. rewrite Rmax_comm -Cmod_opp Copp_minus_distr Rmax_assoc. by apply Rmax_l. apply Hp. apply -> Rminus_le_0 ; apply Hp. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)