proposition: Lemma Cinv_l : forall z : C, z <> C0 -> / z * z = 1.
proof: Proof. intros z z_neq ; destruct z as (r, r0) ; apply (proj1 (Ceq _ _)) ; split ; compute. replace (r * / (r * r + r0 * r0) * r + - (- r0 * / (r * r + r0 * r0) * r0))%R with (((r * r) + - (- r0 * r0)) / (r * r + r0 * r0))%R. unfold Rdiv ; replace (- (- r0 * r0))%R with (r0 * r0)%R by field. apply Rinv_r. intro Hyp ; apply z_neq. apply (proj2 (C0_norm_R0 _)) ; unfold Cnorm_sqr ; intuition. field. replace (r * r + r0 * r0)%R with (Cnorm_sqr (r +i r0)). intro H ; apply z_neq ; apply (proj2 (C0_norm_R0 _) H). unfold Cnorm_sqr ; intuition. field. replace (r * r + r0 * r0)%R with (Cnorm_sqr (r +i r0)). intro H ; apply z_neq ; apply (proj2 (C0_norm_R0 _) H). unfold Cnorm_sqr ; intuition. Qed.
imports: Cdefinitions