proposition: Lemma Cim_le_Cnorm : forall z, Rabs (Cim z) <= Cnorm z.
proof: Proof. intro z ; unfold Cim, Cnorm, Cnorm_sqr ; destruct z. assert (Hrew : forall r, (r*r = r²)%R). intro a ; reflexivity. rewrite <- sqrt_Rsqr_abs. apply sqrt_le_1. intuition (auto with real). apply Rplus_le_le_0_compat ; rewrite Hrew ; intuition (auto with real). apply Rle_trans with (0 + r0²)%R. intuition (auto with real). repeat (rewrite Hrew) ; apply Rplus_le_compat_r ; intuition (auto with real). Qed.
imports: Cbase Cpow