proposition: Lemma unicite_parties_relles_imaginaires : forall (z : C) (a b a' b' : R), z = cons_cart a b -> z = cons_cart a' b' -> a = a' /\ b = b'.
proof: Proof. intros. elim existence_image_complexe with (z := z); intros M H1; try clear existence_image_complexe; try exact H1. apply (unicite_coordonnees (O:=O) (I:=I) (J:=J) (M:=M)); auto with geo. apply complexe_cart_point with z; auto with geo. apply complexe_cart_point with z; auto with geo. Qed.