proposition: Lemma coordonnees_affixe : forall M : PO, cons_cart (abscisse M) (ordonnee M) = affixe M :>C.
proof: Proof. intros. elim existence_affixe_point with (M := M); intros z H; try clear existence_affixe_point; try exact H. elim car_image_forme_algebrique with (z := z) (M := M); [ intros; try exact H1 | eauto with geo ]. rewrite <- H1; rewrite <- H0; rewrite <- H. symmetry in |- *; eauto with geo. Qed.