proposition: Lemma is_gravity_center_col : forall A B C G I, is_gravity_center G A B C -> Midpoint I A B -> Col G I C.
proof: Proof. intros. unfold is_gravity_center in *. spliter. destruct H1 as [J [K [Ha [Hb [Hc Hd]]]]]. elim (three_medians_intersect A B C J K I H);try assumption. intro G';intros. spliter. assert (T:=is_gravity_center_exist_unique A B C H). elim T. intros G''. intros. unfold unique in *. spliter. assert (G''=G). apply H5. unfold is_gravity_center. split;auto. exists J. exists K;auto. assert (G''=G'). apply H5. unfold is_gravity_center. split;auto. exists J. exists K;auto. subst. subst. Col. Qed.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems GeoCoq.Highschool.varignon