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

Section playfair_bis_playfair.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma playfair_bis__playfair : alternative_playfair_s_postulate -> playfair_s_postulate.
Proof.
(* Goal: forall _ : @alternative_playfair_s_postulate Tn, @playfair_s_postulate Tn *)
intros playfair_bis.
(* Goal: @playfair_s_postulate Tn *)
intros A1 A2 B1 B2 C1 C2 P HParAB HPB HParAC HPC.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
elim (col_dec A1 A2 P); [intro HCol; treat_equalities|intro HNC1].

(* Goal: @Perp2 Tn A1 A2 P D P *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  {
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  elim HParAB; [intros [_ [_ [_ HF]]]; exfalso; apply HF; exists P; Col|].
(* Goal: forall _ : and (not (@eq (@Tpoint Tn) A1 A2)) (and (not (@eq (@Tpoint Tn) B1 B2)) (and (@Col Tn A1 B1 B2) (@Col Tn A2 B1 B2))), and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  intros [_ [_ [HCol1 HCol2]]].
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  elim HParAC; [intros [_ [_ [_ HF]]]; exfalso; apply HF; exists P; Col|].
(* Goal: forall _ : and (not (@eq (@Tpoint Tn) A1 A2)) (and (not (@eq (@Tpoint Tn) C1 C2)) (and (@Col Tn A1 C1 C2) (@Col Tn A2 C1 C2))), and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  intros [_ [_ [HCol3 HCol4]]].
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert_diffs; split; ColR.
  }

(* Goal: @Perp2 Tn A1 A2 P D P *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  {
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert_diffs.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert(HX := perp_exists P A1 A2).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  destruct HX as [X HPerp1]; auto.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert_diffs.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert (HCop1 : Coplanar P X A1 A2) by Cop.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  elim (perp_not_col2 _ _ _ _ HPerp1); intro HNC2.

(* Goal: @Perp2 Tn A1 A2 P D P *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    {
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    assert(HD := ex_perp_cop P X P A1).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    destruct HD as [D [HPerp2 HCop2]]; auto.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    assert_diffs.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    assert(Perp2 A1 A2 P D P).
(* Goal: @Perp2 Tn A1 A2 P D P *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
      {
(* Goal: @Perp2 Tn A1 A2 P D P *)
      exists X.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Col Tn P X Y) (and (@Perp Tn X Y A1 A2) (@Perp Tn X Y P D))) *)
      exists P.
(* Goal: and (@Col Tn P X P) (and (@Perp Tn X P A1 A2) (@Perp Tn X P P D)) *)
      split; Col.
(* Goal: and (@Perp Tn X P A1 A2) (@Perp Tn X P P D) *)
      split; Perp.
      }
    assert(Col B1 P D /\ Col B2 P D)
      by (apply (playfair_bis A1 A2 _ _ _ _ P); Col; CopR).
    assert(Col C1 P D /\ Col C2 P D)
      by (apply (playfair_bis A1 A2 _ _ _ _ P); Col; CopR).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    spliter.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    split; apply(col3 P D); Col.
    }

(* Goal: @Perp2 Tn A1 A2 P D P *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    {
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    assert(HD := ex_perp_cop P X P A2).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    destruct HD as [D [HPerp2 HCop2]]; auto.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    assert_diffs.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    assert(Perp2 A1 A2 P D P).
(* Goal: @Perp2 Tn A1 A2 P D P *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
      {
(* Goal: @Perp2 Tn A1 A2 P D P *)
      exists X.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Col Tn P X Y) (and (@Perp Tn X Y A1 A2) (@Perp Tn X Y P D))) *)
      exists P.
(* Goal: and (@Col Tn P X P) (and (@Perp Tn X P A1 A2) (@Perp Tn X P P D)) *)
      split; Col.
(* Goal: and (@Perp Tn X P A1 A2) (@Perp Tn X P P D) *)
      split; Perp.
      }
    assert(Col B1 P D /\ Col B2 P D)
      by (apply (playfair_bis A1 A2 _ _ _ _ P); Col; CopR).
    assert(Col C1 P D /\ Col C2 P D)
      by (apply (playfair_bis A1 A2 _ _ _ _ P); Col; CopR).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    spliter.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    split; apply(col3 P D); Col.
    }
  }
Qed.

End playfair_bis_playfair.