proposition: Lemma triangle_mid_par_flat_cong_aux : forall A B C P Q R, B <> A -> Col A B C -> Midpoint P B C -> Midpoint Q A C -> Midpoint R A B -> Par A B Q P /\ Cong A R P Q /\ Cong B R P Q.
proof: Proof. intros. elim (eq_dec_points A C); intro. assert_all. split; Cong. perm_apply col_par. elim (eq_dec_points B C); intro. assert_all. split; Cong. perm_apply col_par. elim (eq_dec_points A P); intro. assert_all. assert (Col A B Q) by ColR. split. perm_apply col_par. assert_congs_perm. split; Cong. Name x the symmetric of P wrt Q. elim (eq_dec_points P x); intro. treat_equalities; intuition. assert_cols. assert (Parallelogram A P C x) by (apply mid_plg_1 with Q;auto). assert_all. assert_pars_perm. assert (Cong A x B P) by (apply cong_transitivity with P C; Cong). assert (Par A x B P) by (apply par_col2_par with P C; Col; Par). assert (HElim : Parallelogram A x B P \/ Parallelogram A x P B) by (apply par_cong_plg_2; assumption). induction HElim. Name M the intersection of the diagonals (A B) and (x P) of the parallelogram H11. treat_equalities. search_contradiction. assert_paras_perm. assert_pars_perm. assert (Par P Q A B) by (apply par_col_par_2 with x; Col; Par). assert_congs_perm. repeat split; Par; Cong. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec