proposition: Lemma car_image_forme_algebrique : forall (z : C) (M : PO), M = image z -> partie_reelle z = abscisse M /\ partie_imaginaire z = ordonnee M.
proof: Proof. intros. elim existence_coordonnees with (O := O) (I := I) (J := J) (M := M); [ intros x H2; elim H2; intros y H3 | auto with geo ]. cut (z = cons_cart x y); intros. rewrite <- (partie_reelle_def H0). rewrite <- (partie_imaginaire_def H0). split; eauto with geo. eauto with geo. Qed.