proposition: Lemma centre_gravite_prop_vecteur : forall A B C G O : PO, G = centre_gravite A B C -> add_PP (vec O A) (add_PP (vec O B) (vec O C)) = mult_PP 3 (vec O G).
proof: Proof. unfold centre_gravite in |- *; intros. discrimine B C. replace 3 with (1 + 2) by ring. rewrite <- (prop_vecteur_bary (a:=1) (b:=2) (A:=A) (B:=C) (G:=G) O); auto. Ringvec. discrR. rewrite H; rewrite H0; rewrite <- (milieu_trivial C); auto. soit_milieu B C A'. rewrite (prop_vecteur_milieu (B:=B) (C:=C) (A':=A') O); auto. replace 3 with (1 + 2) by ring. rewrite <- (prop_vecteur_bary (a:=1) (b:=2) (A:=A) (B:=A') (G:=G) O); auto. Ringvec. discrR. rewrite H1; auto. Qed.