Require Import GeoCoq.Axioms.beeson_s_axioms.
Require Import GeoCoq.Tarski_dev.Ch08_orthogonality.

Section Tarski_to_intuitionistic_Tarski.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma cong_stability : forall A B C D, ~ ~ Cong A B C D -> Cong A B C D.
Proof.
(* Goal: forall (A A' B B' C C' D D' : @Tpoint Tn) (_ : @Cong Tn A B A' B') (_ : @Cong Tn B C B' C') (_ : @Cong Tn A D A' D') (_ : @Cong Tn B D B' D') (_ : not (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) B C)) (not (BetH A B C))))) (_ : not (and (not (@eq (@Tpoint Tn) A' B')) (and (not (@eq (@Tpoint Tn) B' C')) (not (BetH A' B' C'))))) (_ : not (@eq (@Tpoint Tn) A B)), @Cong Tn C D C' D' *)
intros.
(* Goal: @Cong Tn A B C D *)
elim (cong_dec A B C D); intro HCong.

(* Goal: @Cong Tn A B C D *)
(* Goal: @Cong Tn A B C D *)
  apply HCong.

(* Goal: False *)
  contradiction.
Qed.

Definition BetH A B C : Prop := Bet A B C /\ A <> B /\ B <> C.

Lemma bet_stability : forall A B C, ~ ~ BetH A B C -> BetH A B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (not (BetH A B C))), BetH A B C *)
intros A B C HNNBet.
(* Goal: False *)
unfold BetH in *.
(* Goal: and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C))) *)
elim (bet_dec A B C); intro HBet; elim (eq_dec_points A B); intro HAB; elim (eq_dec_points B C); intro HBC.

(* Goal: False *)
  subst.
(* Goal: @Bet Tn A B C *)
  exfalso.
(* Goal: False *)
  apply HNNBet.
(* Goal: not (@eq (@Tpoint Tn) x A) *)
  intro.
(* Goal: False *)
  spliter.
(* Goal: forall (A B C : @Tpoint Tn) (_ : and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C)))), @Bet Tn A B C *)
  intuition.

(* Goal: False *)
  subst.
(* Goal: @Bet Tn A B C *)
  exfalso.
(* Goal: False *)
  apply HNNBet.
(* Goal: not (@eq (@Tpoint Tn) x A) *)
  intro.
(* Goal: False *)
  spliter.
(* Goal: forall (A B C : @Tpoint Tn) (_ : and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C)))), @Bet Tn A B C *)
  intuition.

(* Goal: False *)
  subst.
(* Goal: @Bet Tn A B C *)
  exfalso.
(* Goal: False *)
  apply HNNBet.
(* Goal: not (@eq (@Tpoint Tn) x A) *)
  intro.
(* Goal: False *)
  spliter.
(* Goal: forall (A B C : @Tpoint Tn) (_ : and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C)))), @Bet Tn A B C *)
  intuition.

(* Goal: and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C))) *)
(* Goal: and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C))) *)
(* Goal: and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C))) *)
(* Goal: and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C))) *)
(* Goal: and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C))) *)
  repeat split; assumption.

(* Goal: @Bet Tn A B C *)
  exfalso.
(* Goal: False *)
  apply HNNBet.
(* Goal: not (@eq (@Tpoint Tn) x A) *)
  intro.
(* Goal: False *)
  spliter.
(* Goal: False *)
  contradiction.

(* Goal: @Bet Tn A B C *)
  exfalso.
(* Goal: False *)
  apply HNNBet.
(* Goal: not (@eq (@Tpoint Tn) x A) *)
  intro.
(* Goal: False *)
  spliter.
(* Goal: False *)
  contradiction.

(* Goal: @Bet Tn A B C *)
  exfalso.
(* Goal: False *)
  apply HNNBet.
(* Goal: not (@eq (@Tpoint Tn) x A) *)
  intro.
(* Goal: False *)
  spliter.
(* Goal: False *)
  contradiction.

(* Goal: @Bet Tn A B C *)
  exfalso.
(* Goal: False *)
  apply HNNBet.
(* Goal: not (@eq (@Tpoint Tn) x A) *)
  intro.
(* Goal: False *)
  spliter.
(* Goal: False *)
  contradiction.
Qed.

Definition T A B C : Prop := ~ (A<>B /\ B<>C /\ ~ BetH A B C).

Definition ColB A B C := ~ (~ T C A B /\ ~ T A C B /\ ~ T A B C).

Lemma between_identity_B : forall A B, ~ BetH A B A.
Proof.
(* Goal: forall A B : @Tpoint Tn, not (BetH A B A) *)
intros A B HNBet.
(* Goal: False *)
unfold BetH in *.
(* Goal: False *)
destruct HNBet as [HBet [HAB HBA]].
(* Goal: False *)
apply between_identity in HBet.
(* Goal: False *)
subst.
(* Goal: forall (A B C : @Tpoint Tn) (_ : and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C)))), @Bet Tn A B C *)
intuition.
Qed.

Lemma Bet_T : forall A B C, Bet A B C -> T A B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C)))), and (@Bet Tn C B A) (and (not (@eq (@Tpoint Tn) C B)) (not (@eq (@Tpoint Tn) B A))) *)
intros A B C HBet.
(* Goal: T A B C *)
unfold T.
(* Goal: not (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) B C)) (not (BetH A B C)))) *)
intro HT.
(* Goal: False *)
destruct HT as [HAB [HBC HNBet]].
(* Goal: False *)
apply HNBet.
(* Goal: forall (A B C : @Tpoint Tn) (_ : BetH A B C), BetH C B A *)
unfold BetH.
(* Goal: forall (A B C : @Tpoint Tn) (_ : and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C)))), @Bet Tn A B C *)
intuition.
Qed.

Lemma BetH_Bet : forall A B C, BetH A B C -> Bet A B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : BetH A B C), BetH C B A *)
unfold BetH.
(* Goal: forall (A B C : @Tpoint Tn) (_ : and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C)))), @Bet Tn A B C *)
intuition.
Qed.

Lemma T_Bet : forall A B C, T A B C -> Bet A B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : T A B C), @Bet Tn A B C *)
intros A B C HT.
(* Goal: @Bet Tn A B C *)
unfold T in HT.
(* Goal: or (T A B C) (not (T A B C)) *)
elim (bet_dec A B C); intro HBet.

(* Goal: not (@Col Tn A B C) *)
  assumption.

(* Goal: @Bet Tn A B C *)
  exfalso.
(* Goal: False *)
  apply HT.
(* Goal: and (not (@eq (@Tpoint Tn) Q x)) (not (@eq (@Tpoint Tn) x A)) *)
  split.

(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (not (BetH A B C)) *)
    intro; subst; apply HBet; apply between_trivial2.

(* Goal: and (not (@eq (@Tpoint Tn) Q x)) (not (@eq (@Tpoint Tn) x A)) *)
    split.

(* Goal: not (@eq (@Tpoint Tn) B C) *)
(* Goal: not (BetH A B C) *)
      intro; subst; apply HBet; apply between_trivial.

(* Goal: not (@Col Tn A B C) *)
      intro HBetH; apply HBet; apply BetH_Bet in HBetH; assumption.
Qed.

Lemma NT_NBet : forall A B C, ~ T A B C -> ~ Bet A B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (T A B C)), not (@Bet Tn A B C) *)
intros A B C HNT.
(* Goal: not (@Bet Tn A B C) *)
intro HNBet.
(* Goal: False *)
apply HNT.
(* Goal: T A B C *)
apply Bet_T.
(* Goal: not (@Col Tn A B C) *)
assumption.
Qed.

Lemma T_dec : forall A B C, T A B C \/ ~ T A B C.
Proof.
(* Goal: forall A B C : @Tpoint Tn, or (T A B C) (not (T A B C)) *)
intros A B C.
(* Goal: or (T A B C) (not (T A B C)) *)
elim (bet_dec A B C); intro HBet.

(* Goal: not (@Col Tn A B C) *)
  left; apply Bet_T; assumption.

(* Goal: not (@Col Tn A B C) *)
  right; intro HT; apply HBet; apply T_Bet in HT; assumption.
Qed.

Lemma between_inner_transitivity_B : forall A B C D : Tpoint, BetH A B D -> BetH B C D -> BetH A B C.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : BetH A B D) (_ : BetH B C D), BetH A B C *)
intros A B C D HBet1 HBet2.
(* Goal: forall (A B C : @Tpoint Tn) (_ : BetH A B C), BetH C B A *)
unfold BetH.
(* Goal: and (not (@eq (@Tpoint Tn) Q x)) (not (@eq (@Tpoint Tn) x A)) *)
repeat split.

(* Goal: @Bet Tn A B C *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
  apply BetH_Bet in HBet1.
(* Goal: @Bet Tn A B C *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
  apply BetH_Bet in HBet2.
(* Goal: not (@Col Tn A B C) *)
  apply between_inner_transitivity with D; assumption.

(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
  unfold BetH in HBet1.
(* Goal: not (@Col Tn A B C) *)
  spliter; assumption.

(* Goal: not (@eq (@Tpoint Tn) B C) *)
  unfold BetH in HBet2.
(* Goal: not (@Col Tn A B C) *)
  spliter; assumption.
Qed.

Lemma ColB_Col : forall A B C, ColB A B C -> Col A B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : ColB A B C), @Col Tn A B C *)
intros A B C HCol.
(* Goal: @Col Tn A B C *)
unfold ColB in HCol.
(* Goal: @Col Tn A B C *)
unfold Col.
elim (T_dec A B C); intro HT1;
elim (T_dec A C B); intro HT2;
elim (T_dec C A B); intro HT3.

(* Goal: forall (A B C : @Tpoint Tn) (_ : and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C)))), @Bet Tn A B C *)
  apply T_Bet in HT1; intuition.

(* Goal: forall (A B C : @Tpoint Tn) (_ : and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C)))), @Bet Tn A B C *)
  apply T_Bet in HT1; intuition.

(* Goal: forall (A B C : @Tpoint Tn) (_ : and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C)))), @Bet Tn A B C *)
  apply T_Bet in HT1; intuition.

(* Goal: forall (A B C : @Tpoint Tn) (_ : and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C)))), @Bet Tn A B C *)
  apply T_Bet in HT1; intuition.

(* Goal: forall (A B C : @Tpoint Tn) (_ : and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C)))), @Bet Tn A B C *)
  apply T_Bet in HT2; intuition.

(* Goal: forall (A B C : @Tpoint Tn) (_ : and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C)))), @Bet Tn A B C *)
  apply T_Bet in HT2; intuition.

(* Goal: forall (A B C : @Tpoint Tn) (_ : and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C)))), @Bet Tn A B C *)
  apply T_Bet in HT3; intuition.

(* Goal: forall (A B C : @Tpoint Tn) (_ : and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C)))), @Bet Tn A B C *)
  exfalso; apply HCol; intuition.
Qed.

Lemma Diff_Col_ColB : forall A B C, Col A B C -> ColB A B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Col Tn A B C), ColB A B C *)
intros A B C H.
(* Goal: ColB A B C *)
unfold Col in H.
(* Goal: ColB A B C *)
unfold ColB.
(* Goal: not (and (not (T C A B)) (and (not (T A C B)) (not (T A B C)))) *)
intro HColB.
(* Goal: False *)
destruct HColB as [HNT1 [HNT2 HNT3]].
(* Goal: False *)
apply NT_NBet in HNT1.
(* Goal: False *)
apply NT_NBet in HNT2.
(* Goal: False *)
apply NT_NBet in HNT3.
(* Goal: False *)
elim H.

(* Goal: False *)
  intro HBet; contradiction.

(* Goal: forall _ : or (@Bet Tn B C A) (@Bet Tn C A B), False *)
  intro HColAux; elim HColAux; intro HBet; clear HColAux.

(* Goal: False *)
(* Goal: False *)
    apply between_symmetry in HBet.
(* Goal: False *)
    contradiction.

(* Goal: False *)
    contradiction.
Qed.

Lemma NColB_NDiffCol : forall A B C, ~ ColB A B C -> ~ Col A B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (ColB A B C)), not (@Col Tn A B C) *)
intros A B C HNCB.
(* Goal: not (@Col Tn A B C) *)
intro HNC.
(* Goal: False *)
apply HNCB.
(* Goal: ColB A B C *)
apply Diff_Col_ColB.
(* Goal: not (@Col Tn A B C) *)
assumption.
Qed.

Lemma NColB_NColOrEq : forall A B C, ~ ColB A B C -> ~ Col A B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (ColB A B C)), not (@Col Tn A B C) *)
intros A B C HNCB.
(* Goal: not (@Col Tn A B C) *)
apply NColB_NDiffCol in HNCB.
(* Goal: not (@Col Tn A B C) *)
assumption.
Qed.

Lemma inner_pasch_B : forall A B C P Q,
  BetH A P C -> BetH B Q C -> ~ ColB A B C ->
  exists x, BetH P x B /\ BetH Q x A.
Proof.
(* Goal: forall (A B C P Q : @Tpoint Tn) (_ : BetH A P C) (_ : BetH B Q C) (_ : not (ColB A B C)), @ex (@Tpoint Tn) (fun x : @Tpoint Tn => and (BetH P x B) (BetH Q x A)) *)
intros A B C P Q HBetH1 HBetH2 HNC.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => and (BetH P x B) (BetH Q x A)) *)
unfold BetH in HBetH1.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => and (BetH P x B) (BetH Q x A)) *)
destruct HBetH1 as [HBet1 [HAP HPC]].
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => and (BetH P x B) (BetH Q x A)) *)
unfold BetH in HBetH2.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => and (BetH P x B) (BetH Q x A)) *)
destruct HBetH2 as [HBet2 [HBQ HQC]].
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => and (BetH P x B) (BetH Q x A)) *)
apply NColB_NColOrEq in HNC.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => and (BetH P x B) (BetH Q x A)) *)
assert (HIP := inner_pasch A B C P Q HBet1 HBet2).
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => and (BetH P x B) (BetH Q x A)) *)
destruct HIP as [x [HBet3 HBet4]].
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => and (BetH P x B) (BetH Q x A)) *)
exists x.
(* Goal: and (not (@eq (@Tpoint Tn) Q x)) (not (@eq (@Tpoint Tn) x A)) *)
split.

(* Goal: not (@Col Tn A B C) *)
  split; try assumption.
(* Goal: and (not (@eq (@Tpoint Tn) Q x)) (not (@eq (@Tpoint Tn) x A)) *)
  split.

(* Goal: not (@eq (@Tpoint Tn) x A) *)
    intro.
(* Goal: False *)
    subst.
(* Goal: False *)
    apply HNC.
(* Goal: @Col Tn A B C *)
    assert_cols.
(* Goal: @Col Tn A B C *)
    ColR.

(* Goal: not (@eq (@Tpoint Tn) x A) *)
    intro.
(* Goal: False *)
    subst.
(* Goal: False *)
    apply HNC.
(* Goal: @Col Tn A B C *)
    assert_cols.
(* Goal: @Col Tn A B C *)
    ColR.

(* Goal: not (@Col Tn A B C) *)
  split; try assumption.
(* Goal: and (not (@eq (@Tpoint Tn) Q x)) (not (@eq (@Tpoint Tn) x A)) *)
  split.

(* Goal: not (@eq (@Tpoint Tn) x A) *)
    intro.
(* Goal: False *)
    subst.
(* Goal: False *)
    apply HNC.
(* Goal: @Col Tn A B C *)
    assert_cols.
(* Goal: @Col Tn A B C *)
    ColR.

(* Goal: not (@eq (@Tpoint Tn) x A) *)
    intro.
(* Goal: False *)
    subst.
(* Goal: False *)
    apply HNC.
(* Goal: @Col Tn A B C *)
    assert_cols.
(* Goal: @Col Tn A B C *)
    ColR.
Qed.

Lemma between_symmetry_B : forall A B C, BetH A B C -> BetH C B A.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : BetH A B C), BetH C B A *)
unfold BetH.
(* Goal: forall (A B C : @Tpoint Tn) (_ : and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C)))), and (@Bet Tn C B A) (and (not (@eq (@Tpoint Tn) C B)) (not (@eq (@Tpoint Tn) B A))) *)
intros A B C HBet.
(* Goal: forall (A B C : @Tpoint Tn) (_ : and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C)))), @Bet Tn A B C *)
repeat split; intuition.
Qed.

Lemma five_segment_B : forall A A' B B' C C' D D' : Tpoint,
    Cong A B A' B' ->
    Cong B C B' C' ->
    Cong A D A' D' ->
    Cong B D B' D' ->
    ~ (A <> B /\ B <> C /\ ~ BetH A B C) ->
    ~ (A' <> B' /\ B' <> C' /\ ~ BetH A' B' C') ->
    A <> B -> Cong C D C' D'.
Proof.
(* Goal: forall (A A' B B' C C' D D' : @Tpoint Tn) (_ : @Cong Tn A B A' B') (_ : @Cong Tn B C B' C') (_ : @Cong Tn A D A' D') (_ : @Cong Tn B D B' D') (_ : not (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) B C)) (not (BetH A B C))))) (_ : not (and (not (@eq (@Tpoint Tn) A' B')) (and (not (@eq (@Tpoint Tn) B' C')) (not (BetH A' B' C'))))) (_ : not (@eq (@Tpoint Tn) A B)), @Cong Tn C D C' D' *)
intros.
(* Goal: @Cong Tn C D C' D' *)
assert (HBet1 : T A B C) by (unfold T; assumption).
(* Goal: @Cong Tn C D C' D' *)
assert (HBet2 : T A' B' C') by (unfold T; assumption).
(* Goal: @Cong Tn C D C' D' *)
apply T_Bet in H3.
(* Goal: @Cong Tn C D C' D' *)
apply T_Bet in H4.
(* Goal: not (@Col Tn A B C) *)
apply five_segment with A A' B B'; assumption.
Qed.

Lemma segment_construction_B : forall A B C D, A<>B -> exists E, T A B E /\ Cong B E C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)), @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (T A B E) (@Cong Tn B E C D)) *)
intros A B C D HDiff.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (T A B E) (@Cong Tn B E C D)) *)
assert (T := segment_construction A B C D).
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (T A B E) (@Cong Tn B E C D)) *)
destruct T as [E [HBet HCong]].
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (T A B E) (@Cong Tn B E C D)) *)
apply Bet_T in HBet.
(* Goal: forall (A B C : @Tpoint Tn) (_ : and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C)))), @Bet Tn A B C *)
exists E; intuition.
Qed.

Lemma lower_dim_B : ~ T PC PA PB /\ ~ T PA PC PB /\ ~ T PA PB PC.
Proof.
(* Goal: and (not (T (@PC Tn) (@PA Tn) (@PB Tn))) (and (not (T (@PA Tn) (@PC Tn) (@PB Tn))) (not (T (@PA Tn) (@PB Tn) (@PC Tn)))) *)
assert (HNBet := lower_dim).
(* Goal: and (not (T (@PC Tn) (@PA Tn) (@PB Tn))) (and (not (T (@PA Tn) (@PC Tn) (@PB Tn))) (not (T (@PA Tn) (@PB Tn) (@PC Tn)))) *)
elim (T_dec PC PA PB); intro HT1; elim (T_dec PA PC PB); intro HT2; elim (T_dec PA PB PC); intro HT3.

(* Goal: not (@Col Tn A B C) *)
  exfalso; apply HNBet; left; apply T_Bet; assumption.

(* Goal: not (@Col Tn A B C) *)
  exfalso; apply HNBet; right; right; apply T_Bet; assumption.

(* Goal: not (@Col Tn A B C) *)
  exfalso; apply HNBet; left; apply T_Bet; assumption.

(* Goal: not (@Col Tn A B C) *)
  exfalso; apply HNBet; right; right; apply T_Bet; assumption.

(* Goal: not (@Col Tn A B C) *)
  exfalso; apply HNBet; left; apply T_Bet; assumption.

(* Goal: not (@Col Tn A B C) *)
  exfalso; apply HNBet; right; left; apply between_symmetry; apply T_Bet; assumption.

(* Goal: not (@Col Tn A B C) *)
  exfalso; apply HNBet; left; apply T_Bet; assumption.

(* Goal: and (not (T (@PC Tn) (@PA Tn) (@PB Tn))) (and (not (T (@PA Tn) (@PC Tn) (@PB Tn))) (not (T (@PA Tn) (@PB Tn) (@PC Tn)))) *)
  tauto.
Qed.

Instance Beeson_follows_from_Tarski : intuitionistic_Tarski_neutral_dimensionless.
Proof.
exact (Build_intuitionistic_Tarski_neutral_dimensionless
 Tpoint BetH Cong
 cong_stability
 bet_stability
 cong_identity
 cong_inner_transitivity
 cong_pseudo_reflexivity
 segment_construction_B
 five_segment_B
 between_identity_B
 between_symmetry_B
 between_inner_transitivity_B
 inner_pasch_B
 PA PB PC
 lower_dim_B).
Qed.

End Tarski_to_intuitionistic_Tarski.