proposition: Lemma centre_gravite_homothetie : forall A B C I G : PO, I = milieu B C :>PO -> G = centre_gravite A B C :>PO -> I = homothetie (- / 2) G A :>PO.
proof: Proof. intros. apply vecteur_homothetie. replace (vec G A) with (mult_PP (-1) (vec A G)). replace (vec G I) with (add_PP (vec A I) (mult_PP (-1) (vec A G))). rewrite (centre_gravite_mediane_vecteur (A:=A) (B:=B) (C:=C) (I:=I) (G:=G)); auto. cut (3 <> 0); intros; auto with real. cut (2 <> 0); intros; auto with real. apply mult_PP_regulier with 2; auto. replace (mult_PP 2 (mult_PP (- / 2) (mult_PP (-1) (mult_PP (/ 3) (mult_PP 2 (vec A I)))))) with (mult_PP (2 * / 2) (mult_PP (/ 3 * 2) (vec A I))). replace (2 * / 2) with 1; auto with real. Fieldvec 3. repeat rewrite mult_mult_vec. replace (2 * / 2 * (/ 3 * 2)) with (2 * (- / 2 * (-1 * (/ 3 * 2)))); auto. field. discrR. Ringvec. Ringvec. Qed.