proposition: Lemma triangle_mid_par_cong_1 : forall A B C P Q R, C <> B -> Midpoint P B C -> Midpoint Q A C -> Midpoint R A B -> Par B C Q R /\ Cong B P Q R .
proof: Proof. intros. split. perm_apply (triangle_mid_par B C A Q R). induction (col_dec A B C). assert (Par C B Q R /\ Cong B P R Q). apply (triangle_mid_par_flat_cong_2 C B A R Q P); Midpoint; Col. spliter. Cong. assert (HTMT := triangle_mid_par_strict_cong A B C P Q R H3 H0 H1 H2); spliter. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec