proposition: Lemma existence_image_vecteur_complexe : forall z : C, exists M : PO, vec O M = image_vec z.
proof: Proof. intros. elim existence_image_complexe with (z := z); intros M H; try clear existence_image_complexe; try exact H. exists M; eauto with geo. Qed.