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

Section SPP_ID.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma strong_parallel_postulate_implies_inter_dec :
  strong_parallel_postulate ->
  decidability_of_intersection.
Proof.
(* Goal: forall _ : @strong_parallel_postulate Tn, @decidability_of_intersection Tn *)
intros HSPP S Q P U.
(* Goal: or (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U)))) *)
elim (col_dec P Q S); intro HPQS; [left; exists P; Col|].
(* Goal: or (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U)))) *)
elim (eq_dec_points P U); intro HPU; treat_equalities; [left; exists Q; Col|].
(* Goal: or (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U)))) *)
assert (H := midpoint_existence P Q); destruct H as [T [HPTQ HCong1]].
(* Goal: or (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U)))) *)
assert (H := symmetric_point_construction S T); destruct H as [R [HRTS HCong2]].
(* Goal: or (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U)))) *)
elim (col_dec P R U); intro HPRU.

(* Goal: or (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U)))) *)
  {
(* Goal: or (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U)))) *)
  assert (HPar : Par_strict Q S P U).
(* Goal: or (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U)))) *)
    {
(* Goal: @Par_strict Tn Q S P U *)
    apply par_strict_col_par_strict with R; Col.
(* Goal: @Par_strict Tn Q S P R *)
    apply par_not_col_strict with P; Col.
(* Goal: @Par Tn Q S P R *)
    apply l12_17 with T; assert_diffs; Col; split; Between; Cong.
    }
(* Goal: or (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U)))) *)
  destruct HPar as [H1 [H2 [H3 H]]].
(* Goal: or (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U)))) *)
  right; intro HI; apply H.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X Q S) (@Col Tn X P U)) *)
  destruct HI as [I [HCol1 HCol2]]; exists I; Col.
  }

(* Goal: or (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U)))) *)
  {
(* Goal: or (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U)))) *)
  elim (cop_dec P Q S U); intro HCop.

(* Goal: or (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U)))) *)
    {
(* Goal: or (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U)))) *)
    assert (H : BetS R T S); try (clear HRTS; rename H into HRTS).
(* Goal: or (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U)))) *)
      {
(* Goal: @BetS Tn R T S *)
      split; Between.
(* Goal: and (not (@eq (@Tpoint Tn) R T)) (not (@eq (@Tpoint Tn) T S)) *)
      split; try (intro; treat_equalities; assert_cols; Col).
      }
(* Goal: or (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U)))) *)
     assert (H : BetS P T Q); try (clear HPTQ; rename H into HPTQ).
(* Goal: or (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U)))) *)
      {
(* Goal: @BetS Tn P T Q *)
      split; Col.
(* Goal: and (not (@eq (@Tpoint Tn) P T)) (not (@eq (@Tpoint Tn) T Q)) *)
      split; try (intro; treat_equalities; Col).
      }
    assert (HI := HSPP P Q R S T U); destruct HI as [I [HCol1 HCol2]]; Cong;
    try (left; exists I; Col).
(* Goal: @Coplanar Tn P Q R U *)
    unfold BetS in *; spliter.
(* Goal: @Coplanar Tn P Q R U *)
    apply coplanar_trans_1 with S; [Col|exists T; right; right; split; Col|Cop].
    }

(* Goal: or (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U)))) *)
    {
(* Goal: or (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I S Q) (@Col Tn I P U)))) *)
    right; intros [I []].
(* Goal: False *)
    apply HCop.
(* Goal: @BetS Tn P T Q *)
    exists I; right; right; split; Col.
    }
  }
Qed.

End SPP_ID.