proposition: Lemma Cnorm_mult : forall lambda : R, forall z : C, Cnorm (lambda `* z) = ((Rabs lambda) * (Cnorm z))%R.
proof: Proof. intros lambda z ; destruct z as (r1, r2) ; unfold Cnorm ; unfold Cnorm_sqr ; simpl. replace (lambda * r1 * (lambda * r1) + lambda * r2 * (lambda * r2))%R with (lambda^2 * (r1 * r1 + r2 * r2))%R by ring. rewrite sqrt_mult ; assert (sqrt (lambda ^ 2) = Rabs lambda)%R as H0. rewrite <- sqrt_Rsqr_abs ; simpl ; unfold Rsqr ; rewrite Rmult_1_r ; reflexivity. rewrite H0 ; reflexivity. simpl ; rewrite Rmult_1_r ; apply sqrt_Rsqr_abs. simpl ; rewrite Rmult_1_r ; apply Rle_0_sqr. simpl ; rewrite Rmult_1_r ; apply sqrt_Rsqr_abs. apply Rplus_le_le_0_compat ; apply Rle_0_sqr. Qed.
imports: Cbase Cpow