proposition: Lemma module_Conj : forall z : C, module (Conj z) = module z.
proof: Proof. intros. elim existence_parties_relles_imaginaires with (z := z); intros x H; elim H; intros y H0; try clear H; try exact H0. cut (Conj z = cons_cart x (- y)); intros. rewrite (passage_algebrique_module H); rewrite (passage_algebrique_module H0). replace (Rsqr (- y)) with (Rsqr y); [ auto | unfold Rsqr in |- *; ring ]. apply Conj_def; auto. Qed.