proposition: Lemma complex_triangle_diameter_corner (a b c : C) : forall z, complex_triangle a b c z -> Cmod (z - a) <= complex_triangle_diameter a b c.
proof: Proof. intros _ [x [y [z [Hx [ Hy [ Hz [H ->]]]]]]]. rewrite !scal_R_Cmult. case: (Req_dec y 1) => Hb. rewrite Hb {y Hb Hy} in H |- *. assert (x = 0). apply Rle_antisym => //. apply Rplus_le_reg_r with (1 + z)%R. rewrite -Rplus_assoc H. by apply Rminus_le_0 ; ring_simplify. rewrite H0 {x H0 Hx} in H |- *. assert (z = 0). replace z with ((0 + 1 + z)%R - 1)%R by ring. rewrite H ; ring. rewrite H0 !Cmult_0_l Cmult_1_l Cplus_0_l Cplus_0_r. eapply Rle_trans, Rmax_r. by apply Rmax_l. assert (x + z <> 0)%R. contradict Hb. replace y with ((x + y + z) - (x + z))%R by ring. by rewrite Hb Rminus_0_r H. eapply Rle_trans. apply (complex_triangle_diameter_segment a b (scal (x / (x + z))%R a + scal (z / (x + z))%R c)). exists (x + z)%R ; split. split. by apply Rplus_le_le_0_compat. by rewrite -H ; apply Rminus_le_0 ; ring_simplify. rewrite -H !scal_R_Cmult RtoC_minus !RtoC_div // !RtoC_plus. field ; contradict H0 ; by injection H0. rewrite /complex_triangle_diameter. apply Rmax_le_compat. rewrite !scal_R_Cmult !RtoC_div // !RtoC_plus. replace (a - (x / (x + z) * a + z / (x + z) * c)) with (z / (x + z) * (a - c)). 2: field ; contradict H0 ; by injection H0. rewrite Cmod_mult -!RtoC_plus -RtoC_div // Cmod_R. rewrite -{2}(Rmult_1_l (Cmod _)) ; apply Rmult_le_compat_r. by apply Cmod_ge_0. rewrite Rabs_div // !Rabs_pos_eq //. 2: by apply Rplus_le_le_0_compat. apply -> Rdiv_le_1. apply Rminus_le_0 ; by ring_simplify. assert (0 <= x + z) by now apply Rplus_le_le_0_compat. by apply sym_not_eq in H0 ; case: H1 => H1. apply Rmax_case. by apply Rmax_l. rewrite !scal_R_Cmult !RtoC_div // !RtoC_plus. replace (x / (x + z) * a + z / (x + z) * c - b) with (x / (x + z) * (a - b) + z / (x + z) * (c - b)). 2: field ; contradict H0 ; by injection H0. eapply Rle_trans. eapply Rle_trans, Rplus_le_compat. apply Cmod_triangle. rewrite Cmod_mult -!RtoC_plus -RtoC_div // Cmod_R. apply Rmult_le_compat_l. by apply Rabs_pos. rewrite -Cmod_opp Copp_minus_distr. apply (Rmax_l _ (Cmod (c - b))). rewrite Cmod_mult -!RtoC_plus -RtoC_div // Cmod_R. apply Rmult_le_compat_l. by apply Rabs_pos. apply (Rmax_r (Cmod (b - a))). rewrite -Rmult_plus_distr_r. rewrite !Rabs_pos_eq. replace (x / (x + z) + z / (x + z))%R with 1 by now field. rewrite Rmult_1_l ; apply Rle_refl. apply Rdiv_le_0_compat => //. assert (0 <= x + z) by now apply Rplus_le_le_0_compat. by apply sym_not_eq in H0 ; case: H1 => H1. apply Rdiv_le_0_compat => //. assert (0 <= x + z) by now apply Rplus_le_le_0_compat. by apply sym_not_eq in H0 ; case: H1 => H1. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)