proposition: Lemma Cnorm_Cmult : forall z1 z2, Cnorm (z1 * z2) = (Cnorm z1 * Cnorm z2)%R.
proof: Proof. intros z1 z2 ; destruct z1 as (a,b) ; destruct z2 as (c,d) ; unfold Cnorm ; unfold Cnorm_sqr ; simpl. replace ((a * c - b * d) * (a * c - b * d) + (a * d + b * c) * (a * d + b * c))%R with ((a * a + b * b) * (c * c + d * d))%R by field. apply sqrt_mult ; apply Rplus_le_le_0_compat ; apply Rle_0_sqr. Qed.
imports: Cbase Cpow