proposition: Lemma centre_gravite_mediane_vecteur : forall A B C I G : PO, I = milieu B C :>PO -> G = centre_gravite A B C :>PO -> vec A G = mult_PP (/ 3) (mult_PP 2 (vec A I)) :>PP.
proof: Proof. unfold centre_gravite in |- *; intros. rewrite <- H in H0. cut (3 <> 0); intros; auto with real. apply mult_PP_regulier with 3; auto. replace 3 with (1 + 2) by ring. rewrite <- (prop_vecteur_bary (a:=1) (b:=2) (A:=A) (B:=I) (G:=G) A); auto. Fieldvec 3. Qed.