proposition: Lemma is_gravity_center_exist_unique : forall A B C, ~ Col A B C -> exists! G, is_gravity_center G A B C.
proof: Proof. Proof with finish. intros. assert_diffs. Name I the midpoint of B and C. Name J the midpoint of A and C. elim (intersection_two_medians_exist A B C I J H H1 H4); intros G HG; spliter. exists G; unfold unique; unfold is_gravity_center; repeat split... exists I; exists J; do 3 (split; finish). intros G' HG'; spliter; decompose [ex and] H8;clear H8. assert_all. apply l6_21 with A x B x0... intro;search_contradiction. show_distinct' B x0... Qed.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems GeoCoq.Highschool.varignon