proposition: Lemma droite_milieu : forall A B C I J : PO, I = milieu A B -> J = milieu A C -> mult_PP 2 (vec I J) = vec B C.
proof: Proof. intros. rewrite H0; rewrite H. VReplace (mult_PP 2 (vec (milieu A B) (milieu A C))) (add_PP (mult_PP (-1) (cons 2 (milieu A B))) (cons 2 (milieu A C))). repeat rewrite <- add_PP_milieu. Ringvec. Qed.