proposition: Lemma egalite_vecteur_point : forall A B C : PO, vec C A = vec C B :>PP -> A = B :>PO.
proof: Proof. intros. apply vecteur_nul_conf. replace (vec A B) with (add_PP (vec C B) (mult_PP (-1) (vec C A))); [ idtac | Ringvec ]. rewrite H; Ringvec. Qed.