proposition: Lemma Cmod_conj_compat : forall z, Cre (z * Cconj z) = ((Cnorm z) ^ 2)%R /\ Cim ( z * Cconj z) = 0%R.
proof: Proof. intros z. split ; CusingR1. unfold Cnorm. rewrite Rmult_1_r. rewrite <- sqrt_mult. rewrite sqrt_square. unfold Cnorm_sqr. simpl. ring. apply Cnorm_sqr_pos. apply Cnorm_sqr_pos. apply Cnorm_sqr_pos. Qed.
imports: Ctacfield Cbase Cpow Lia