proposition: Lemma triangle_mid_par_cong : forall A B C P Q R, B <> A -> C <> A -> C <> B -> Midpoint P B C -> Midpoint Q A C -> Midpoint R A B -> Par A B Q P /\ Par A C P R /\ Par B C Q R /\ Cong A R P Q /\ Cong B R P Q /\ Cong A Q P R /\ Cong C Q P R /\ Cong B P Q R /\ Cong C P Q R.
proof: Proof. intros. elim (col_dec A B C); intro. apply triangle_mid_par_flat_cong; assumption. assert (HTMT := triangle_mid_par_strict_cong A B C P Q R H5 H2 H3 H4); spliter. repeat split; try apply par_strict_par; assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec