proposition: Lemma sesamath_4ieme_G2_ex45 : forall A B C I K J M G, ~ Col A B C -> Midpoint I B C -> Col I A M -> Midpoint A I M -> Midpoint J A I -> Par J K A C -> Col K I C -> Col G C A /\ Col G M K -> Midpoint K I C /\ Par A K M C /\ is_gravity_center G C M I.
proof: Proof. intros. assert_diffs. assert_cols. assert (~ Col C I A) by (intro;apply H;ColR). spliter. split. assert(Midpoint K C I). (apply(triangle_par_mid C A I J K);finish). finish. destruct (eq_dec_points I M). { treat_equalities. intuition. } assert (~ Col I M C) by (intro;apply H14;ColR). assert_diffs. assert(Midpoint K C I). (apply(triangle_par_mid C A I J K);finish). split. assert(Par M C A K) by(apply(triangle_mid_par M C I K A);finish). Par. exists. assert(~ Col C M I);finish. exists A. exists K. split. assert(Midpoint A M I);finish. repeat split;finish. Qed.
imports: GeoCoq.Highschool.triangles GeoCoq.Highschool.circumcenter GeoCoq.Highschool.gravityCenter