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