proposition: Lemma passage_algebrique_module : forall (z : C) (x y : R), z = cons_cart x y -> module z = sqrt (Rsqr x + Rsqr y).
proof: Proof. intros. elim existence_image_complexe with (z := z); intros M H2; try clear existence_image_complexe; try exact H2. replace (module z) with (distance O M); auto. rewrite (distance_coordonnees (O:=O) (I:=I) (J:=J) (M:=M) (x:=x) (y:=y)); eauto with geo. symmetry in |- *; eauto with geo. Qed.