proposition: Lemma sesamath_4ieme_G2_ex37 : forall S E L I M A O, ~Col S E L -> Midpoint I L S -> Midpoint M S E -> Midpoint A E L -> Perp_bisect A O L E -> Coplanar S E L O -> Perp A O I M.
proof: Proof. intros. assert_diffs. assert_cols. assert (Par L E I M) by (perm_apply (triangle_mid_par L E S M I);finish). assert (Perp A O L E) by(apply(perp_bisect_perp A O L E);finish). assert (Perp I M O A). apply(cop_par_perp__perp L E I M O A);Perp; CopR. assert (Perp A O I M);finish. Qed.
imports: GeoCoq.Highschool.triangles GeoCoq.Highschool.circumcenter GeoCoq.Highschool.gravityCenter