Require Import GeoCoq.Axioms.parallel_postulates.
Require Import GeoCoq.Tarski_dev.Ch05_bet_le.

Section tarski_s_euclid_remove_degenerated_cases.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma tarski_s_euclid_remove_degenerated_cases :
  (forall A B C D T,
   A <> B ->
   A <> C ->
   A <> D ->
   A <> T ->
   B <> C ->
   B <> D ->
   B <> T ->
   C <> D ->
   C <> T ->
   D <> T ->
   ~ Col A B C ->
   Bet A D T ->
   Bet B D C ->
   exists x y : Tpoint, Bet A B x /\ Bet A C y /\ Bet x T y) ->
  forall A B C D T,
  Bet A D T ->
  Bet B D C ->
  A <> D -> exists x y : Tpoint, Bet A B x /\ Bet A C y /\ Bet x T y.
Proof.
(* Goal: forall (_ : forall (A B C D T : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) A C)) (_ : not (@eq (@Tpoint Tn) A D)) (_ : not (@eq (@Tpoint Tn) A T)) (_ : not (@eq (@Tpoint Tn) B C)) (_ : not (@eq (@Tpoint Tn) B D)) (_ : not (@eq (@Tpoint Tn) B T)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@eq (@Tpoint Tn) C T)) (_ : not (@eq (@Tpoint Tn) D T)) (_ : not (@Col Tn A B C)) (_ : @Bet Tn A D T) (_ : @Bet Tn B D C), @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y))))) (A B C D T : @Tpoint Tn) (_ : @Bet Tn A D T) (_ : @Bet Tn B D C) (_ : not (@eq (@Tpoint Tn) A D)), @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
intro HGC; intros A B C D T HADT HBDC HAD.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
elim (eq_dec_points A B); intro HAB.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
subst; exists T; exists C; Between.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
elim (eq_dec_points A C); intro HAC.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
subst; exists B; exists T; Between.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
elim (eq_dec_points A T); intro HAT.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
exfalso; apply HAD; treat_equalities; reflexivity.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
elim (eq_dec_points B C); intro HBC.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
subst; exists T; exists T; Between.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
elim (eq_dec_points B D); intro HBD.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
subst; exists T; exists C; Between.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
elim (eq_dec_points B T); intro HBT.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
subst; exists T; exists C; Between.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
elim (eq_dec_points C D); intro HCD.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
subst; exists B; exists T; Between.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
elim (eq_dec_points C T); intro HCT.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
subst; exists B; exists T; Between.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
elim (eq_dec_points D T); intro HDT.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
subst; exists B; exists C; Between.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
elim (col_dec A B C); intro HABC.

(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
  {
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
  elim HABC; clear HABC; intro HABC.

(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
    {
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
    assert (H : Bet A B D) by eBetween; assert (Bet A B T) by eBetween.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
    exists T; exists C; Between.
    }

(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
    {
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
    elim HABC; clear HABC; intro HABC.

(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
      {
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
      assert (H : Bet A C D) by eBetween; assert (Bet A C T) by eBetween.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
      exists B; exists T; Between.
      }

(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
      {
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
      assert (H : Bet B A D \/ Bet B D A) by (apply l5_3 with C; Between).
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
      elim H; clear H; intro H.

(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
        {
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
        assert (H' : Bet A C T \/ Bet A T C) by (apply l5_2 with B; eBetween).
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
        elim H'; clear H'; intro H'.

(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
          {
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
          exists B; exists T; Between.
          }

(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
          {
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
          exists B; exists C; split ; try Between.
(* Goal: and (@Bet Tn A C C) (@Bet Tn B T C) *)
          split; try Between.
(* Goal: @Bet Tn B T C *)
          eBetween.
          }
        }
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
        {
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
        assert (H' : Bet A B T \/ Bet A T B) by (apply l5_1 with D; Between).
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
        elim H'; clear H'; intro H'.

(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
          {
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
          exists T; exists C; Between.
          }

(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
          {
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
          exists B; exists C; split ; try Between.
(* Goal: and (@Bet Tn A C C) (@Bet Tn B T C) *)
          split; try Between.
(* Goal: @Bet Tn B T C *)
          eBetween.
          }
        }
      }
    }
  }
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
  {
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
  apply HGC with D; assumption.
  }
Qed.

End tarski_s_euclid_remove_degenerated_cases.