proposition: Lemma centre_gravite_intersection_trois_medianes : forall A B C I J K G : PO, triangle A B C -> I = milieu B C :>PO -> J = milieu A B :>PO -> K = milieu A C :>PO -> G = centre_gravite A B C :>PO -> G = pt_intersection (droite A I) (droite B K) :>PO /\ G = pt_intersection (droite A I) (droite C J) :>PO.
proof: Proof. intros. split; [ idtac | try assumption ]. apply centre_gravite_intersection_medianes with (B := C); auto with geo. rewrite H3; auto with geo. apply centre_gravite_intersection_medianes with (B := B); auto. Qed.