proposition: Lemma centre_gravite_intersection_medianes : forall A B C I J G : PO, triangle A B C -> I = milieu B C :>PO -> J = milieu A B :>PO -> G = centre_gravite A B C :>PO -> G = pt_intersection (droite A I) (droite C J) :>PO.
proof: Proof. intros. deroule_triangle A B C. cut (triangle B C A); auto with geo; unfold triangle in |- *; intros. cut (C <> J); intros. cut (A <> I); intros. cut (3 <> 0); intros; auto with real. replace (droite C J) with (droite J C); auto with geo. apply def_pt_intersection; auto. left. apply triangle_medianes_triangle with (1 := H); auto. apply colineaire_alignes with (/ 3 * 2); auto. rewrite (centre_gravite_mediane_vecteur (A:=A) (B:=B) (C:=C) (I:=I) (G:=G)); auto. Fieldvec 3. apply permute_alignes; auto. apply colineaire_alignes with (/ 3 * 2); auto. rewrite (centre_gravite_mediane_vecteur (A:=C) (B:=A) (C:=B) (I:=J) (G:=G)); auto. Fieldvec 3. rewrite H2; auto with geo. rewrite H0. apply triangle_milieu_distinct; auto. rewrite H1. apply triangle_milieu_distinct; auto. Qed.