proposition: Lemma carre_module : forall (z : C) (x y : R), z = cons_cart x y -> Rsqr (module z) = Rsqr x + Rsqr y.
proof: Proof. intros. rewrite (passage_algebrique_module H). rewrite Rsqr_sqrt; auto. assert (0 <= Rsqr x); auto with real. assert (0 <= Rsqr y); auto with real. lra. Qed.