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

Section tarski_euclid.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma tarski_s_euclid_implies_euclid_5 :
  tarski_s_parallel_postulate ->
  euclid_5.
Proof.
(* Goal: forall _ : @tarski_s_parallel_postulate Tn, @euclid_5 Tn *)
intros HT P Q R S T U HPTQ HRTS HQUR HNC HCong1 HCong2.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@BetS Tn S Q I) (@BetS Tn P U I)) *)
destruct (symmetric_point_construction R P) as [V HMid].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@BetS Tn S Q I) (@BetS Tn P U I)) *)
assert (Hc1 : Bet V P R) by (unfold Midpoint in *; spliter; Between).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@BetS Tn S Q I) (@BetS Tn P U I)) *)
assert (Hc2 : Bet Q U R) by (unfold BetS in *; spliter; Between).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@BetS Tn S Q I) (@BetS Tn P U I)) *)
destruct (inner_pasch V Q R P U) as [W [HPWQ HUWV]]; Col; clear Hc1; clear Hc2.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@BetS Tn S Q I) (@BetS Tn P U I)) *)
assert (HPW : P <> W).
(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
  {
(* Goal: not (@eq (@Tpoint Tn) P W) *)
  intro; treat_equalities.
(* Goal: False *)
  assert (P <> V).
(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
    {
(* Goal: not (@eq (@Tpoint Tn) P V) *)
    intro; treat_equalities; apply HNC; unfold BetS in *; spliter; assert_cols; ColR.
    }
  apply HNC; apply BetSEq in HPTQ; apply BetSEq in HRTS; apply BetSEq in HQUR;
(* Goal: @Col Tn P R X *)
  spliter; assert_cols; ColR.
  }
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@BetS Tn S Q I) (@BetS Tn P U I)) *)
destruct (HT P V U W Q) as [X [Y [HPVX [HPUY HXQY]]]]; Between.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@BetS Tn S Q I) (@BetS Tn P U I)) *)
assert (HPar : Par_strict Q S P R).
(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
  {
(* Goal: @Par_strict Tn Q S P R *)
  apply par_not_col_strict with P; Col.
  assert_diffs; unfold BetS in *; spliter;
  apply l12_17 with T; try split; Cong; Between.
  }
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@BetS Tn S Q I) (@BetS Tn P U I)) *)
assert (HTS : TS Q S P Y).
(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
  {
(* Goal: @TS Tn Q S P Y *)
  apply l9_8_2 with X.

(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
    {
(* Goal: @TS Tn Q S X Y *)
    assert_diffs.
    assert (P <> R)
      by (intro; treat_equalities; apply par_strict_distinct in HPar; spliter; Col).
    assert (P <> X)
      by (intro; treat_equalities; apply par_strict_distinct in HPar; spliter; Col).
(* Goal: @TS Tn Q S X Y *)
    assert (~ Col X Q S).
(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
      {
(* Goal: not (@Col Tn X Q S) *)
      apply par_strict_not_col_2 with P.
(* Goal: @Par_strict Tn P X Q S *)
      apply par_strict_symmetry; apply par_strict_col_par_strict with R; Col.
      unfold BetS in *; unfold Midpoint in *; spliter;
(* Goal: @Col Tn P R X *)
      assert_diffs; assert_cols; ColR.
      }
(* Goal: @TS Tn Q S X Y *)
    repeat split; try (exists Q); Col.
(* Goal: not (@Col Tn Y Q S) *)
    intro HCol.
    assert (Q = Y)
      by (apply l6_21 with Q S X Q; try (intro; treat_equalities); Col).
(* Goal: False *)
    treat_equalities.
(* Goal: False *)
    assert (Q = U).
(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
      {
      apply BetSEq in HPTQ; apply BetSEq in HRTS; apply BetSEq in HQUR;
      spliter; apply l6_21 with Q P R Q; Col.
(* Goal: not (@Col Tn Q P R) *)
      apply par_strict_not_col_2 with S; Par.
      }
(* Goal: False *)
    treat_equalities; unfold BetS in *; spliter; Col.
    }

(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
    {
    assert (P <> R)
      by (intro; treat_equalities; apply par_strict_distinct in HPar; spliter; Col).
    assert (P <> V)
      by (intro; treat_equalities; apply par_strict_distinct in HPar; spliter; Col).
    assert (P <> X)
      by (intro; treat_equalities; apply par_strict_distinct in HPar; spliter; Col).
    apply l12_6; apply par_strict_right_comm;
    apply par_strict_col_par_strict with R; Col.
(* Goal: @Col Tn P R X *)
    assert_cols; ColR.
    }
  }
destruct HTS as [Hc1 [Hc2 [I [HCol HBet]]]];
clear Hc1; clear Hc2; exists I.
(* Goal: and (@BetS Tn S Q I) (@BetS Tn P U I) *)
assert (HPUI : BetS P U I).
(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
 {
  assert (P <> Y)  by (intro; treat_equalities; Col).
(* Goal: @BetS Tn P U I *)
  assert (HPUI : Col P U I) by (assert_cols; ColR).
(* Goal: @BetS Tn S Q I *)
  split.

(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
    {
(* Goal: @Bet Tn P U I *)
    elim HPUI; clear HPUI; intro HPUI; Col.
(* Goal: @Bet Tn P U I *)
    elim HPUI; clear HPUI; intro HPUI; exfalso.

(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
      {
(* Goal: False *)
      assert (HFalse : TS Q S P U).
(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
        {
(* Goal: and (@BetS Tn S Q I) (@BetS Tn P U I) *)
        split; Col.
(* Goal: and (not (@Col Tn U Q S)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T Q S) (@Bet Tn P T U))) *)
        split; try (exists I; split; Col; Between).
(* Goal: not (@Col Tn U P R) *)
        intro.
(* Goal: False *)
        assert (Q = U).
(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
          {
          apply BetSEq in HPTQ; apply BetSEq in HRTS; apply BetSEq in HQUR;
(* Goal: @eq (@Tpoint Tn) Q U *)
          spliter; apply l6_21 with S Q R Q; Col.
(* Goal: not (@Col Tn Q S R) *)
          apply par_strict_not_col_1 with P; Par.
          }
(* Goal: False *)
        treat_equalities; unfold BetS in *; spliter; intuition.
        }
(* Goal: False *)
      apply l9_9 in HFalse; apply HFalse.
(* Goal: @OS Tn Q S P U *)
      apply one_side_transitivity with R.

(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
        {
(* Goal: @OS Tn Q S P R *)
        apply l12_6; Col.
        }

(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
        {
        apply BetSEq in HPTQ; apply BetSEq in HRTS; apply BetSEq in HQUR;
        spliter; assert_diffs; assert_cols; apply l9_19 with Q; Col.
(* Goal: and (@BetS Tn S Q I) (@BetS Tn P U I) *)
        repeat split; Col.
(* Goal: not (@Col Tn Q S R) *)
        apply par_strict_not_col_1 with P; Par.
        }
      }

(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
      {
(* Goal: False *)
      assert (HFalse : TS P R I U).
(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
        {
(* Goal: @TS Tn P R I U *)
        split; try (intro; apply HPar; exists I; Col).
(* Goal: and (not (@Col Tn U P R)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T P R) (@Bet Tn I T U))) *)
        split; try (exists P; split; Col; Between).
(* Goal: not (@Col Tn U P R) *)
        intro.
(* Goal: False *)
        assert (R = U).
(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
          {
(* Goal: @eq (@Tpoint Tn) R U *)
          unfold BetS in *; spliter; apply l6_21 with P R Q U; Col.
(* Goal: not (@Col Tn P R Q) *)
          apply par_strict_not_col_1 with S; Par.
          }
(* Goal: False *)
        treat_equalities; unfold BetS in *; spliter; intuition.
        }
(* Goal: False *)
      apply l9_9 in HFalse; apply HFalse.
(* Goal: @OS Tn P R I U *)
      apply one_side_transitivity with Q.

(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
        {
        apply l12_6; apply par_strict_right_comm;
        apply par_strict_col_par_strict with S; Par; Col.
        intro; treat_equalities;
        apply BetSEq in HPTQ; apply BetSEq in HRTS; apply BetSEq in HQUR; spliter;
(* Goal: @Col Tn P R X *)
        apply HNC; assert_cols; ColR.
        }

(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
        {
(* Goal: @OS Tn P R Q U *)
        assert (HPar':= HPar); apply par_strict_distinct in HPar.
        apply BetSEq in HPTQ; apply BetSEq in HRTS; apply BetSEq in HQUR;
        spliter; assert_diffs; assert_cols; apply l9_19 with R; Col.
(* Goal: and (@Out Tn R Q U) (not (@Col Tn P R Q)) *)
        repeat split; Between.
(* Goal: not (@Col Tn P R Q) *)
        apply par_strict_not_col_3 with S; Par.
        }
      }
    }

(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
    {
    split; try (intro; treat_equalities; apply par_strict_not_col_3 in HPar;
                apply BetSEq in HPTQ; apply BetSEq in HRTS; apply BetSEq in HQUR;
                spliter; assert_cols; Col).
(* Goal: False *)
    try (intro; treat_equalities; Col).
(* Goal: False *)
    assert (Q = U).
(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
      {
(* Goal: @eq (@Tpoint Tn) Q U *)
      apply l6_21 with S Q R Q; Col.
(* Goal: not (@Col Tn P Q R) *)
(* Goal: not (@Col Tn I Q R) *)
      intro; apply HNC; ColR.
      }
(* Goal: False *)
    treat_equalities; unfold BetS in *; spliter; intuition.
    }
 }
(* Goal: and (@BetS Tn S Q I) (@BetS Tn P U I) *)
split; Col.
(* Goal: @BetS Tn S Q I *)
assert (HTS : TS Q R S I).
(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
  {
(* Goal: @TS Tn Q R S I *)
  apply l9_8_2 with P.

(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
    {
    apply BetSEq in HPTQ; apply BetSEq in HRTS; apply BetSEq in HQUR;
(* Goal: @TS Tn Q S X Y *)
    apply BetSEq in HPUI; spliter; assert_diffs.
(* Goal: @TS Tn Q R P I *)
    assert_cols; repeat split; try (exists U; Col).
(* Goal: not (@Col Tn P Q R) *)
(* Goal: not (@Col Tn I Q R) *)
    intro; apply HNC; ColR.
(* Goal: not (@Col Tn I Q R) *)
    intro; apply par_strict_not_col_4 in HPar; apply HPar; ColR.
    }

(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
    {
(* Goal: @OS Tn Q R P S *)
    apply l12_6.
    apply par_not_col_strict with P; Col;
    try (intro; apply par_strict_not_col_3 in HPar; Col).
    apply BetSEq in HPTQ; apply BetSEq in HRTS; apply BetSEq in HQUR;
    assert_diffs; spliter;
    apply l12_17 with T; try split; Cong; Between.
    }
  }
(* Goal: @BetS Tn S Q I *)
split.

(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
  {
(* Goal: @Bet Tn S Q I *)
  elim HCol; intro HSQI; Between.
(* Goal: @Bet Tn S Q I *)
  assert (HFalse := HTS).
(* Goal: @Bet Tn S Q I *)
  apply l9_9 in HFalse; exfalso; apply HFalse.
  apply BetSEq in HPTQ; apply BetSEq in HRTS; apply BetSEq in HQUR;
  spliter; apply l9_19 with Q; Col.
(* Goal: and (@BetS Tn S Q I) (@BetS Tn P U I) *)
  apply par_strict_not_col_4 in HPar; split; Col.
(* Goal: @Out Tn Q S I *)
  unfold TS in HTS; spliter; assert_diffs; repeat split; elim HSQI; Between.
  }

(* Goal: and (not (@eq (@Tpoint Tn) S Q)) (not (@eq (@Tpoint Tn) Q I)) *)
  {
  assert (HFalse := HTS); unfold TS in HTS; spliter;
  assert_diffs; repeat split; Col; intro; treat_equalities;
  assert (HTS := not_two_sides_id S Q R); Col.
  }
Qed.

End tarski_euclid.