proposition: Lemma triangle_par_mid : forall A B C P Q, ~ Col A B C -> Midpoint P B C -> Par A B Q P -> Col Q A C -> Midpoint Q A C.
proof: Proof. assert (H:=playfair_s_postulate_implies_midpoint_converse_postulate); unfold midpoint_converse_postulate in H; intros; apply H with B P; Col. unfold playfair_s_postulate. apply parallel_uniqueness. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec