proposition: Lemma produit_Conj_module : forall z : C, Cmult z (Conj z) = Rinj (Rsqr (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. pattern z at 1 2 in |- *. rewrite H0. rewrite Conj_algebrique. rewrite (passage_algebrique_module H0). rewrite Cmult_algebrique. RReplace (y * x + x * - y) 0. rewrite Rsqr_sqrt. unfold Rsqr, Rinj in |- *. RReplace (x * x + - (y * - y)) (x * x + y * y); auto. assert (0 <= Rsqr x); auto with real. assert (0 <= Rsqr y); auto with real. lra. Qed.