proposition: Lemma gravity_center_change_triangle: forall A B C G I B' C', is_gravity_center G A B C -> Midpoint I B C -> Midpoint I B' C' -> ~ Col A B' C' -> is_gravity_center G A B' C'.
proof: Proof. intros. Name G' the midpoint of A and G. assert (Midpoint G I G') by (apply (is_gravity_center_third A B C G G' I);finish). apply (is_gravity_center_third_reci A B' C' G I G');finish. Qed.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems GeoCoq.Highschool.circumcenter GeoCoq.Highschool.orthocenter GeoCoq.Highschool.midpoint_thales GeoCoq.Highschool.concyclic GeoCoq.Highschool.gravityCenter