proposition: Lemma milieu_vecteur : forall A B M : PO, M = milieu A B :>PO -> vec A M = vec M B.
proof: Proof. intros. rewrite H. apply mult_PP_regulier with 2; auto with real. VReplace (mult_PP 2 (vec A (milieu A B))) (add_PP (cons (-2) A) (cons 2 (milieu A B))). VReplace (mult_PP 2 (vec (milieu A B) B)) (mult_PP (-1) (add_PP (cons 2 (milieu A B)) (cons (-2) B))). rewrite <- add_PP_milieu; RingPP. Qed.