proposition: Lemma sesamath_4ieme_G2_ex36_aux : forall A B C I J K, ~ Col A B C -> Midpoint I A B -> Midpoint J A C -> Midpoint K B C -> Plg I J K B.
proof: Proof. intros. assert_diffs. assert (Par A B J K) by (perm_apply (triangle_mid_par B A C J K)). assert (Par B I J K) by (apply par_col_par_2 with A;finish). assert (Par B C I J) by (perm_apply (triangle_mid_par B C A J I)). assert (Par B K I J) by (apply par_col_par_2 with C;finish). assert (~ Col B K J) by (intro;apply H;ColR). assert (Par_strict B K I J) by (apply par_not_col_strict with J;finish). assert (Plg I J K B) by (apply pars_par_plg;finish). assumption. Qed.
imports: GeoCoq.Highschool.triangles GeoCoq.Highschool.circumcenter GeoCoq.Highschool.gravityCenter