proposition: Lemma C0_norm_R0 : forall z, z = 0 <-> Cnorm_sqr z = 0%R.
proof: Proof. intro z ; unfold Cnorm_sqr ; split ; intro Hrew. destruct (proj2 (Ceq z 0) Hrew) as (H1, H2) ; destruct z as (r1,r2); simpl in * ; rewrite H1 ; rewrite H2 ; field. apply (proj1 (Ceq _ _)) ; split. apply Rsqr_0_uniq. apply Rplus_eq_0_l with ((Cim z)²)%R ; [apply Rle_0_sqr | apply Rle_0_sqr |]. unfold Rsqr. assumption. destruct z as (a,b) ; intuition. simpl in *. apply Rsqr_0_uniq. apply Rplus_eq_0_l with ((a)²)%R ; [apply Rle_0_sqr | apply Rle_0_sqr |]. unfold Rsqr. rewrite Rplus_comm. assumption. Qed.
imports: Cdefinitions