proposition: Lemma triangle_mid_par_strict_cong_simp : 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. apply triangle_mid_par. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec