proposition: Lemma Cnorm_triang : forall z1 z2 : C, Cnorm (z1 + z2) <= (Cnorm z1 + Cnorm z2)%R.
proof: Proof. destruct z1 as (r0, r1) ; destruct z2 as (r2, r3) ; simpl ; apply Rsqr_incr_0. unfold Cnorm. unfold Cnorm_sqr. simpl. rewrite Rsqr_plus ; repeat (rewrite Rsqr_sqrt) ; [| apply Rplus_le_le_0_compat ; apply Rle_0_sqr | apply Rplus_le_le_0_compat ; apply Rle_0_sqr |]. assert (H : 0 <= (r0 * r3 - r1 * r2) * (r0 * r3 - r1 * r2)) by (apply Rle_0_sqr). assert (2 * r0 * r2 * r1 * r3 <= (r0 * r3) * (r0 * r3) + (r1 * r2) * (r1 * r2))%R as H1. ring_simplify in H ; ring_simplify ; apply Rminus_le ; apply Ropp_le_ge_contravar in H ; rewrite Ropp_0 in H. assert (H0 : (-(r0^2 * r3^2 - 2 * r0 * r3 * r1 * r2 + r1^2 * r2^2) = 2 * r0 * r2 * r1 * r3 - (r0^2 * r3^2 + r2^2 * r1^2))%R). ring. rewrite <- H0 ; intuition (auto with real). ring_simplify ; repeat (rewrite Rplus_assoc) ; apply Rplus_le_compat_l. rewrite Rplus_comm ; rewrite Rplus_assoc ; apply Rplus_le_compat_l ; rewrite Rplus_assoc ; apply Rplus_le_compat_l ; rewrite Rplus_assoc ; rewrite Rplus_comm ; rewrite Rplus_assoc ; apply Rplus_le_compat_l ; apply Rsqr_incr_0_var. repeat (rewrite Rsqr_mult ; rewrite Rsqr_sqrt) ; [| apply Rplus_le_le_0_compat ; apply Rle_0_sqr | apply Rplus_le_le_0_compat ; apply Rle_0_sqr]. rewrite Rsqr_plus ; ring_simplify. assert (Temp : (Rsqr (2 * r0 * r2) = r0^2 * r2^2 * (Rsqr 2))%R). compute ; ring. rewrite <- Temp ; clear Temp. assert (Temp : (Rsqr (2 * r1 * r3) = r1^2 * r3^2 * Rsqr 2)%R). compute ; ring. rewrite <- Temp ; clear Temp. repeat rewrite Rplus_assoc ; apply Rplus_le_compat_l ; rewrite Rplus_comm ; repeat rewrite <- Rplus_assoc ; apply Rplus_le_compat_r ; replace 8%R with (4 * 2)%R by ring ; replace (Rsqr 2)%R with 4%R by intuition ; rewrite <- Rmult_plus_distr_r ; rewrite Rmult_assoc ; rewrite Rmult_assoc ; rewrite Rmult_assoc ; rewrite Rmult_assoc ; rewrite Rmult_comm ; apply Rmult_le_compat_r ; [lra |]. ring_simplify ; ring_simplify in H1 ; exact H1. rewrite Rmult_assoc ; apply Rmult_le_pos ; [lra |] ; apply Rmult_le_pos ; apply sqrt_positivity ; apply Rplus_le_le_0_compat ; apply Rle_0_sqr. apply Rplus_le_le_0_compat ; apply Rle_0_sqr. apply sqrt_positivity; apply Rplus_le_le_0_compat ; apply Rle_0_sqr. apply Rplus_le_le_0_compat ; apply sqrt_positivity ; apply Rplus_le_le_0_compat ; apply Rle_0_sqr. Qed.
imports: Cbase Cpow