proposition: Lemma complex_triangle_diameter_le (a b c z0 z : C) : complex_triangle a b c z0 -> complex_triangle a b c z -> Cmod (z - z0) <= complex_triangle_diameter a b c.
proof: Proof. case => {z0} x0 [y0 [z0 [Hx0 [ Hy0 [ Hz0 [H0 ->]]]]]]. case => {z} x' [y' [z' [Hx' [ Hy' [ Hz' [H' ->]]]]]]. case: (Req_dec x0 1) => Ha0. replace (scal x0 a + scal y0 b + scal z0 c) with a. apply (complex_triangle_diameter_corner a b c). by exists x', y', z'. rewrite Ha0 scal_one Rplus_assoc -{2}(Rplus_0_r 1) {x0 Ha0 Hx0} in H0 |- *. apply Rplus_eq_reg_l in H0. replace y0 with 0. replace z0 with 0. rewrite !scal_zero_l. change zero with (RtoC 0). by rewrite !Cplus_0_r. eapply sym_eq, Rplus_eq_0_l => //. 2: erewrite Rplus_comm ; apply H0. by []. eapply sym_eq, Rplus_eq_0_l => //. 2: apply H0. by []. rewrite !scal_R_Cmult. wlog: x' y' z' x0 y0 z0 Hx' Hy' Hz' H' Hx0 Hy0 Hz0 H0 Ha0 / (x0 <= x') => [Hw | Ha]. case: (Rle_lt_dec x0 x') => Ha. by apply Hw. rewrite -Cmod_opp Copp_minus_distr. apply Hw => //. eapply Rlt_not_eq, Rlt_le_trans. by apply Ha. rewrite -H0 Rminus_le_0 ; ring_simplify. by apply Rplus_le_le_0_compat. by apply Rlt_le. assert (y0 + z0 <> 0)%R. contradict Ha0. rewrite -H0 Rplus_assoc Ha0 ; ring. assert (0 < y0 + z0). assert (0 <= y0 + z0) by now apply Rplus_le_le_0_compat. case: H1 => // H1. by apply sym_eq in H1. assert (y' + z' <= y0 + z0). replace (y' + z')%R with (1 - x')%R by (rewrite -H' ; ring). replace (y0 + z0)%R with (1 - x0)%R by (rewrite -H0 ; ring). apply Rplus_le_compat_l. by apply Ropp_le_contravar. wlog: b c x0 y0 z0 x' y' z' Hx0 Hy0 Hz0 Hx' Hy' Hz' H' H0 Ha Ha0 H2 H H1 / (x0 = 0) => [Hw | {Hx0 Ha} Hx0]. set (b' := scal x0 a + scal (y0 + z0)%R b). set (c' := scal x0 a + scal (y0 + z0)%R c). eapply Rle_trans. eapply Rle_trans, (Hw b' c' 0 (y0 / (y0 + z0))%R (z0 / (y0 + z0))%R (x' - x0 * (y' + z') / (y0 + z0))%R (y' / (y0 + z0))%R (z' / (y0 + z0))%R) => //. apply Req_le ; apply f_equal. rewrite /b' /c' !scal_R_Cmult RtoC_minus !RtoC_div // RtoC_mult !RtoC_plus. field. by contradict H ; injection H. by apply Rle_refl. apply Rdiv_le_0_compat => //. apply Rdiv_le_0_compat => //. rewrite -Rminus_le_0 -(Rmult_1_r x') /Rdiv Rmult_assoc. apply Rmult_le_compat => //. apply Rdiv_le_0_compat => //. by apply Rplus_le_le_0_compat. apply -> Rdiv_le_1 => //. apply Rdiv_le_0_compat => //. apply Rdiv_le_0_compat => //. replace x0 with (1 - (y0 + z0))%R by (rewrite -H0 ; ring). replace x' with (1 - (y' + z'))%R by (rewrite -H' ; ring). now field. now field. rewrite -Rminus_le_0 -(Rmult_1_r x') /Rdiv Rmult_assoc. apply Rmult_le_compat => //. apply Rdiv_le_0_compat => //. by apply Rplus_le_le_0_compat. apply -> Rdiv_le_1 => //. by apply Rlt_not_eq, Rlt_0_1. rewrite /Rdiv -!Rmult_plus_distr_r. apply Rmult_le_compat_r => //. by apply Rlt_le, Rinv_0_lt_compat. replace (y0 / (y0 + z0) + z0 / (y0 + z0))%R with 1 by now field. by apply Rgt_not_eq, Rlt_0_1. replace (y0 / (y0 + z0) + z0 / (y0 + z0))%R with 1 by now field. by apply Rlt_0_1. rewrite /complex_triangle_diameter /c' /b' !scal_R_Cmult RtoC_plus. replace (a - (x0 * a + (y0 + z0) * c)) with ((y0 + z0) * (a - c)). replace (x0 * a + (y0 + z0) * b - a) with ((y0 + z0) * (b - a)). replace (x0 * a + (y0 + z0) * c - (x0 * a + (y0 + z0) * b)) with ((y0 + z0) * (c - b)) by ring. rewrite !Cmod_mult -RtoC_plus Cmod_R. rewrite !RmaxRmult ; try by apply Rabs_pos. rewrite -{2}(Rmult_1_l (Rmax _ _)). apply Rmult_le_compat_r. eapply Rle_trans, Rmax_l ; apply Cmod_ge_0. rewrite Rabs_pos_eq. by rewrite Rminus_le_0 -H0 ; ring_simplify. by apply Rlt_le. replace x0 with (1 - (y0 + z0))%R by (rewrite -H0 ; ring). rewrite RtoC_minus RtoC_plus ; ring. replace x0 with (1 - (y0 + z0))%R by (rewrite -H0 ; ring). rewrite RtoC_minus RtoC_plus ; ring. rewrite Hx0 Cmult_0_l Cplus_0_l Rplus_0_l {x0 Hx0 Ha0 H H1} in H0 |- *. clear H2. wlog: b c y' z' y0 z0 Hy' Hz' H' Hy0 Hz0 H0 / ((y' + z') * y0 <= y') => [Hw | Hab]. case: (Rle_lt_dec ((y' + z') * y0)%R y') => Hab. by apply Hw. rewrite complex_triangle_diameter_swap. rewrite -Cplus_assoc !(Cplus_comm (_ * b)) Cplus_assoc. apply Hw => //. rewrite -H' ; ring. by rewrite Rplus_comm. rewrite Rplus_comm. pattern z' at 2 ; replace z' with ((y' + z') - y')%R by ring. replace z0 with (1 - y0)%R by (rewrite -H0 ; ring). rewrite Rmult_plus_distr_l Rmult_1_r. apply Rplus_le_compat_l. apply Ropp_le_cancel ; rewrite Ropp_involutive. eapply Rlt_le, Rlt_le_trans. apply Hab. apply Req_le ; ring. assert (Hac : z' <= (y' + z') * z0). pattern z' at 1 ; replace z' with ((y' + z') - y')%R by ring. replace z0 with (1 - y0)%R by (rewrite -H0 ; ring). rewrite Rmult_plus_distr_l Rmult_1_r. apply Rplus_le_compat_l. apply Ropp_le_cancel ; rewrite Ropp_involutive. eapply Rle_trans, Hab. apply Req_le ; ring. case: (Req_dec y0 1) => Hb. replace (y0 * b + z0 * c) with b. rewrite complex_triangle_diameter_turn. apply complex_triangle_diameter_corner. exists y', z', x' ; repeat split => //. rewrite -H' ; ring. rewrite !scal_R_Cmult ; ring. unfold complex_triangle_diameter. replace z0 with (1 - y0)%R by (rewrite -H0 ; ring). rewrite RtoC_minus Hb ; ring. assert (Hc : (z0 <> 0)%R). contradict Hb ; rewrite -H0 Hb ; ring. wlog: c y0 z0 y' z' Hy0 Hz0 H0 Hy' Hz' H' Hab Hac Hb Hc / (z0 = 1) => [Hw | {Hc} Hc]. set (c' := (y0 * b + z0 * c)). eapply Rle_trans. eapply Rle_trans, (Hw c' 0 1) => //. rewrite /c' Cmult_plus_distr_l Cplus_assoc !Cmult_assoc. rewrite -(Cplus_assoc _ (_ * b) (_*b)) -Cmult_plus_distr_r. instantiate (2 := (z' / z0)%R). replace ((z' / z0)%R * z0) with (RtoC z'). 2: rewrite RtoC_div // ; now field ; contradict Hc ; injection Hc. replace ((z' / z0)%R * y0) with (z' / z0 - RtoC z'). 2: replace y0 with (1 - z0)%R by (rewrite -H0 ; ring). 2: rewrite RtoC_div // RtoC_minus ; now field ; contradict Hc ; injection Hc. instantiate (1 := (y' - (z' / z0 - z'))%R). apply Req_le, f_equal. rewrite !RtoC_minus RtoC_div // ; ring. by apply Rle_refl. by apply Rle_0_1. ring. rewrite -Rminus_le_0 Rle_minus_l Rle_div_l //. apply sym_not_eq in Hc ; by case: Hz0. apply Rdiv_le_0_compat => //. apply sym_not_eq in Hc ; case: Hz0 => //. rewrite -H' ; ring. rewrite Rmult_0_r. rewrite -Rminus_le_0 Rle_minus_l Rle_div_l //. apply sym_not_eq in Hc ; by case: Hz0. rewrite Rmult_1_r. rewrite -Rle_minus_l Rminus_eq_0 -Rminus_le_0 Rle_minus_l Rle_div_l //. apply sym_not_eq in Hc ; by case: Hz0. by apply Rlt_not_eq, Rlt_0_1. by apply Rgt_not_eq, Rlt_0_1. rewrite /complex_triangle_diameter /c'. apply Rmax_case. replace (a - (y0 * b + z0 * c)) with (y0 * (a - b) + z0 * (a - c)). 2: replace y0 with (1 - z0)%R by (rewrite -H0 ; ring). 2: rewrite RtoC_minus ; ring. eapply Rle_trans. eapply Rle_trans, Rplus_le_compat. apply Cmod_triangle. rewrite Cmod_mult Cmod_R -Cmod_opp Copp_minus_distr. apply Rmult_le_compat_l. by apply Rabs_pos. apply (Rmax_r (Cmod (a - c))). rewrite Cmod_mult Cmod_R. apply Rmult_le_compat_l. by apply Rabs_pos. apply (Rmax_l _ (Cmod (b - a))). rewrite -Rmult_plus_distr_r. rewrite !Rabs_pos_eq // H0 Rmult_1_l. rewrite Rmax_assoc ; apply Rmax_l. apply Rmax_case. eapply Rle_trans, Rmax_r. apply Rmax_l. replace (y0 * b + z0 * c - b) with (z0 * (c - b)). 2: replace y0 with (1 - z0)%R by (rewrite -H0 ; ring). 2: rewrite RtoC_minus ; ring. rewrite Cmod_mult Cmod_R. eapply Rle_trans, Rmax_r. eapply Rle_trans, Rmax_r. rewrite -{2}(Rmult_1_l (Cmod _)). apply Rmult_le_compat_r. by apply Cmod_ge_0. rewrite Rabs_pos_eq // -H0 Rminus_le_0 ; by ring_simplify. replace (y0 * b + z0 * c) with c. 2: replace y0 with (1 - z0)%R by (rewrite -H0 ; ring). 2: rewrite Hc Rminus_eq_0 ; ring. rewrite -complex_triangle_diameter_turn. apply (complex_triangle_diameter_corner c a b). exists z', x', y' ; repeat split => //. rewrite -H' ; ring. rewrite !scal_R_Cmult ; ring. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)