proposition: Lemma prop_vecteur_bary : forall (a b : R) (A B G M : PO), a + b <> 0 -> G = barycentre (cons a A) (cons b B) -> add_PP (mult_PP a (vec M A)) (mult_PP b (vec M B)) = mult_PP (a + b) (vec M G).
proof: Proof. intros. apply add_PP_vecteur; auto. rewrite (add_PP_barycentre (a:=a) (b:=b) A B); auto. rewrite <- H0; auto. Qed.