proposition: Lemma existence_parties_relles_imaginaires : forall z : C, exists a : R, (exists b : R, z = cons_cart a b).
proof: Proof. intros. elim existence_image_complexe with (z := z); intros M H1; try clear existence_image_complexe; try exact H1. elim existence_coordonnees with (O := O) (I := I) (J := J) (M := M); [ intros x H2; elim H2; intros y H3 | auto with geo ]. exists x; exists y. apply (cart_point_complexe (z:=z) (a:=x) (b:=y) (M:=M)); auto with geo. Qed.