proposition: Lemma Cnorm_sqr_real : forall r9 r10, (r9 +i r10) <> 0 -> ((r9 + r9) * (r9 + r9) + (r10 + r10) * (r10 + r10))%R <> 0%R.
proof: Proof. intros a b H Habs. apply (HC0_norm_R0 ((a + a)%R +i (b + b)%R)) in Habs. apply H. replace ((a + a)%R +i (b + b)%R) with ((2 +i 0%R) * (a +i b)) in Habs by CusingR_f. apply Cmult_integral in Habs. destruct Habs ; assert (H1 : (2 +i 0%R) = 0 -> False) ; CusingR2 ; (lra || intuition). Qed.
imports: Complex Cpow_plus