proposition: Lemma is_gravity_center_coplanar : forall A B C G, is_gravity_center G A B C -> Coplanar G A B C.
proof: Proof. intros. destruct H as [HNCol [I [J]]]; spliter. exists I; left; split; Col. Qed.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems GeoCoq.Highschool.varignon