proposition: Lemma sesamath_4ieme_G2_ex40 : forall A B C M R N S T, ~Col A B C -> Bet C R B -> Midpoint M A B -> Midpoint N A C -> Midpoint S B R -> Midpoint T R C -> Par M S N T /\ Parallelogram M S T N.
proof: Proof. intros. assert_diffs. assert_cols. assert_all_diffs_by_contradiction. assert (Par A R M S) by (perm_apply (triangle_mid_par A R B S M);finish). assert (Par A R N T) by (perm_apply (triangle_mid_par A R C T N);finish). assert(Par M S N T) by (perm_apply(par_trans M S A R);finish). split. assumption. assert(Par C B N M) by (perm_apply (triangle_mid_par B C A N M);finish). destruct (eq_dec_points R B). { treat_equalities. assert(Plg M N T S) by(apply(sesamath_4ieme_G2_ex36_aux A S C M N T);finish). assert(Parallelogram M N T S) by(apply(plg_to_parallelogram M N T S);finish). apply(Plg_perm M N T S);finish. } destruct (eq_dec_points R C). { treat_equalities. assert(Plg N M S T) by(apply(sesamath_4ieme_G2_ex36_aux A T B N M S);finish). assert(Parallelogram N M S T) by(apply(plg_to_parallelogram N M S T);finish). apply(Plg_perm N M S T);finish. } assert_all_diffs_by_contradiction. assert(Par M N B R) by(apply(par_col_par M N B C R);finish). assert(Par M N R S) by(apply(par_col_par M N R B S);finish). assert(Par M N S T) by(apply(par_col_par M N S R T);finish;ColR). assert (~Col M S T) by (intro;apply H;ColR). apply(par_2_plg);finish. Qed.
imports: GeoCoq.Highschool.triangles GeoCoq.Highschool.circumcenter GeoCoq.Highschool.gravityCenter