Require Import GeoCoq.Axioms.parallel_postulates.
Require Import GeoCoq.Tarski_dev.Definitions.

Section playfair_existential_playfair.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma playfair__existential_playfair :
  playfair_s_postulate ->
  existential_playfair_s_postulate.
Proof.
(* Goal: forall _ : @playfair_s_postulate Tn, @existential_playfair_s_postulate Tn *)
intro HF.
(* Goal: @existential_playfair_s_postulate Tn *)
exists PA, PB, PC.
(* Goal: and (not (@Col Tn (@PA Tn) (@PB Tn) (@PC Tn))) (forall (B1 B2 C1 C2 : @Tpoint Tn) (_ : @Par Tn (@PA Tn) (@PB Tn) B1 B2) (_ : @Col Tn (@PC Tn) B1 B2) (_ : @Par Tn (@PA Tn) (@PB Tn) C1 C2) (_ : @Col Tn (@PC Tn) C1 C2), and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2)) *)
split; [apply lower_dim|]; intros; apply HF with PA PB PC; assumption.
Qed.

End playfair_existential_playfair.