proposition: Lemma Cnorm_le_Cre_Cim : forall z, Cnorm z <= Rabs (Cre z) + Rabs (Cim z).
proof: Proof. intro z ; unfold Cnorm, Cnorm_sqr ; destruct z as (a,b) ; simpl. rewrite <- sqrt_square. apply sqrt_le_1. apply Rplus_le_le_0_compat ; apply Rle_0_sqr. apply Rmult_le_pos ; apply Rplus_le_le_0_compat ; apply Rabs_pos. apply Rle_trans with (Rabs a * Rabs a + Rabs b * Rabs b)%R. repeat rewrite <- Rabs_mult. apply Rplus_le_compat ; apply RRle_abs. rewrite Rmult_plus_distr_r ; repeat rewrite Rmult_plus_distr_l. repeat (rewrite Rplus_assoc) ; apply Rplus_le_compat_l. apply Rle_trans with (0 + Rabs b * Rabs b)%R ; [intuition (auto with real) |]. rewrite <- Rplus_assoc ; apply Rplus_le_compat_r ; apply Rplus_le_le_0_compat ; apply Rmult_le_pos ; apply Rabs_pos. apply Rplus_le_le_0_compat ; apply Rabs_pos. Qed.
imports: Cbase Cpow