proposition: Lemma triangle_mid_par_strict : forall A B C P Q, ~Col A B C -> Midpoint P B C -> Midpoint Q A C -> Par_strict A B Q P.
proof: Proof. intros. Name x the symmetric of P wrt Q. assert_all. assert (~ Col A P C) by (intro; apply H; ColR). assert_diffs. assert (Parallelogram_strict A P C x) by (apply mid_plgs with Q;auto). assert (Cong A x B P) by CongR. assert (Par A x B P) by (assert_pars_perm; apply par_col2_par with P C; Col). assert (HElim : Parallelogram A x B P \/ Parallelogram A x P B) by (apply par_cong_plg_2; assumption). induction HElim. assert_paras_perm; assert_pars_perm. Name M the intersection of the diagonals (A B) and (x P) of the parallelogram H15. treat_equalities. search_contradiction. apply par_strict_col2_par_strict with x P; Col. assert_diffs; auto. apply ncol123_plg__pars1423; auto; intro; apply H. assert (P <> x) by (intro; treat_equalities; Col). apply col_permut231; apply col123_124__col234 with P; [| |apply col_permut231]; Col. apply col_permut231; apply col123_124__col134 with Q; Col. apply col_permut231; apply col123_124__col134 with x; Col. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec