Require Import GeoCoq.Axioms.parallel_postulates.
Require Import GeoCoq.Tarski_dev.Ch12_parallel.

Section par_trans_playfair.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma par_trans_implies_playfair :
  postulate_of_transitivity_of_parallelism -> playfair_s_postulate.
Proof.
(* Goal: forall _ : @postulate_of_transitivity_of_parallelism Tn, @playfair_s_postulate Tn *)
intros HPT A1; intros.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
assert (Par C1 C2 B1 B2) by (apply HPT with A1 A2; Par).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
induction H3.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
exfalso; apply H3; exists P; Col.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
spliter; split; Col.
Qed.

End par_trans_playfair.