proposition: Lemma sesamath_4ieme_G2_ex38 : forall E A U M N L, ~ Col E A U -> Midpoint N E A -> Midpoint M E U -> Midpoint L U A -> exists O : Tpoint, Col O E L /\ Midpoint O M N.
proof: Proof. intros. assert_diffs. assert_cols. assert( ~Col U E A);finish. assert (Plg M L N E) by (apply (sesamath_4ieme_G2_ex36_aux U E A M L N);finish). assert (Parallelogram M L N E) by (apply(plg_to_parallelogram M L N E);finish). assert (exists X, Midpoint X M N /\ Midpoint X L E) by (apply plg_mid;finish). destruct H18 as [X [HX HX2]]. exists X. assert_cols;split;finish. Qed.
imports: GeoCoq.Highschool.triangles GeoCoq.Highschool.circumcenter GeoCoq.Highschool.gravityCenter