proposition: Lemma milieu_vecteur_double : forall A B M : PO, M = milieu A B :>PO -> vec A B = mult_PP 2 (vec A M) :>PP.
proof: Proof. intros. VReplace (vec A B) (add_PP (vec A M) (vec M B)). rewrite <- (milieu_vecteur (A:=A) (B:=B) (M:=M)); auto. Ringvec. Qed.