fact: Definition is_gravity_center G A B C := ~ Col A B C /\ exists I, exists J, Midpoint I B C /\ Midpoint J A C /\ Col G A I /\ Col G B J.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems GeoCoq.Highschool.varignon