proposition: Lemma egalite_vecteur_OM_image : forall (z z' : C) (M M' : PO), z = affixe_vec (vec O M) :>C -> z' = affixe_vec (vec O M') :>C -> vec O M = vec O M' :>PP -> z = z' :>C.
proof: Proof. intros. apply egalite_point_image with (M := M) (M' := M'); eauto with geo. apply vecteur_nul_conf. replace (vec M M') with (add_PP (vec O M') (mult_PP (-1) (vec O M))); [ idtac | Ringvec ]. rewrite H1; Ringvec. Qed.