Library GeoCoq.Meta_theory.Parallel_postulates.playfair_midpoint

Require Import GeoCoq.Axioms.parallel_postulates.
Require Import GeoCoq.Tarski_dev.Ch13_1.

Section playfair_midpoints.

Context `{T2D:Tarski_2D}.

Lemma playfair_s_postulate_implies_midpoint_converse_postulate :
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.
 apply l6_21 with A C P Q.
  assert (Col A B C) by ColR.
  assert (Par A B Q P A B Q P) by (apply par_distincts; finish).
  spliter; intuition.
  destruct (HP A B Q P X P P) as [HCol1 HCol2]; Col; apply par_strict_par; Par.
treat_equalities; assumption.

End playfair_midpoints.