proposition: Lemma Cnorm_0 : forall z : C, Cnorm z = 0%R -> z = C0.
proof: Proof. intros z Hz ; destruct z as (a, b) ; apply (proj2 (C0_norm_R0 _)). apply sqrt_eq_0 ; [| assumption] ; apply Rplus_le_le_0_compat ; apply Rle_0_sqr. Qed.
imports: Cbase Cpow