proposition: Lemma egalite_affixe_vecteur_OM : forall (z z' : C) (M M' : PO), z = affixe_vec (vec O M) :>C -> z' = affixe_vec (vec O M') :>C -> z = z' :>C -> vec O M = vec O M' :>PP.
proof: Proof. intros. replace M' with M; auto. apply egalite_affixe_point with (3 := H1); auto with geo. Qed.