proposition: Lemma playfair_s_postulate_implies_midpoint_converse_postulate : playfair_s_postulate -> midpoint_converse_postulate.
proof: Proof. intros HP A; intros. destruct (midpoint_existence A C) as [X HAC]. assert (X = Q). assert (Par_strict A B X P). apply triangle_mid_par with C; assumption. assert_diffs. assert_cols. apply l6_21 with A C P Q. intro. assert (Col A B C) by ColR. contradiction. auto. Col. Col. destruct (HP A B Q P X P P) as [HCol1 HCol2]; Col; apply par_strict_par; Par. Col. treat_equalities; assumption. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Ch13_1