proposition: Lemma sesamath_4ieme_G2_ex47 : forall A B C A' B' C', ~Col A C C' -> ~Col A A' C'-> Col B' A' C' -> Midpoint B A C-> Par A A' B B' -> Par A A' C C' -> Midpoint B' A' C'.
proof: Proof. intros. assert_diffs. assert_cols. destruct (midpoint_existence A C') as [x Hx]. assert_cols. assert(Par B B' A A');finish. assert(Par B B' C C') by(apply(par_trans B B' A A' C C');finish;Par). assert(Par C C' B x) by(apply(triangle_mid_par C C' A x B);finish). assert(Par B B' B x) by(apply(par_trans B B' C C' B x);finish). assert(Col B B' x) by(apply(par_id B B' x);finish). assert( Par A A' B x) by(apply(par_trans A A' B B' B x);finish). assert_diffs. assert(x=B'\/x<>B') by(apply(eq_dec_points x B');finish). destruct H14. destruct H14. assert(Col A C' A') by(apply(l6_16_1 C' x A' A);finish;Par). destruct H0. assert(Col A A' C');finish. assert(Par B x B' B);finish. assert(Par B x B' x) by(apply(par_col_par B x B' B x);finish). assert( Par A A' B' x) by(apply(par_trans A A' B x B' x);finish). assert(Midpoint B' A' C') by(apply(triangle_par_mid A' A C' x B');finish). assumption. Qed.
imports: GeoCoq.Highschool.triangles GeoCoq.Highschool.circumcenter GeoCoq.Highschool.gravityCenter