proposition: Lemma Cnorm_inv : forall z : C, z <> 0 -> Cnorm (/z) = (/(Cnorm z))%R.
proof: Proof. intros z Hz ; unfold Cnorm, Cnorm_sqr ; destruct z as (a,b). simpl. replace ((a / (a * a + b * b) * (a / (a * a + b * b)) + - b / (a * a + b * b) * (- b / (a * a + b * b))))%R with (1 / (a * a + b * b))%R. rewrite <- Rmult_1_l ; rewrite <- sqrt_1 at 2 ; rewrite sqrt_div. reflexivity. intuition (auto with real). case (Req_or_neq a) ; intro Ha. case (Req_or_neq b) ; intro Hb. destruct Hz ; subst ; reflexivity. apply Rplus_le_lt_0_compat ; [apply Rle_0_sqr | apply Rlt_0_sqr ; assumption]. apply Rplus_lt_le_0_compat ; [apply Rlt_0_sqr ; assumption | apply Rle_0_sqr]. field ; case (proj1 (C0_neq_R0_neq _) Hz) ; unfold Cre ; simpl ; intro H. apply Rgt_not_eq ; apply Rplus_lt_le_0_compat ; [apply Rlt_0_sqr ; assumption | apply Rle_0_sqr]. apply Rgt_not_eq ; apply Rplus_le_lt_0_compat ; [apply Rle_0_sqr | apply Rlt_0_sqr ; assumption]. Qed.
imports: Cbase Cpow