proposition: Lemma prop_vecteur_milieu : forall B C A' O : PO, A' = milieu B C :>PO -> add_PP (vec O B) (vec O C) = mult_PP 2 (vec O A').
proof: Proof. unfold milieu in |- *; intros. replace 2 with (1 + 1) by ring. rewrite <- (prop_vecteur_bary (a:=1) (b:=1) (A:=B) (B:=C) (G:=A') O); auto. Ringvec. lra. Qed.