Require Import GeoCoq.Axioms.beeson_s_axioms.
Require Import GeoCoq.Axioms.tarski_axioms.

Section Proof_of_eq_stability_in_IT.

Context `{BTn:intuitionistic_Tarski_neutral_dimensionless}.

Lemma cong_stability_eq_stability : forall A B : ITpoint, ~ A <> B -> A = B.
Proof.
(* Goal: forall (A B : @ITpoint BTn) (_ : not (not (@eq (@ITpoint BTn) A B))), @eq (@ITpoint BTn) A B *)
intros A B HAB.
(* Goal: @eq (@ITpoint BTn) A B *)
apply Icong_identity with A.
(* Goal: @ICong BTn A B A A *)
apply Cong_stability.
(* Goal: not (not (@ICong BTn A B A A)) *)
intro HNCong.
(* Goal: False *)
apply HAB.
(* Goal: not (@eq (@ITpoint BTn) A B) *)
intro HEq.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
subst.
(* Goal: False *)
apply HNCong.
(* Goal: @ICong BTn B B B B *)
apply Icong_pseudo_reflexivity.
Qed.

End Proof_of_eq_stability_in_IT.

Require Import Classical.

Section Intuitionistic_Tarski_to_Tarski.

Context `{BTn:intuitionistic_Tarski_neutral_dimensionless}.

Lemma col_dec : forall A B C, ICol A B C \/ ~ ICol A B C.
Proof.
(* Goal: forall A B : @ITpoint BTn, or (@eq (@ITpoint BTn) A B) (not (@eq (@ITpoint BTn) A B)) *)
intros.
(* Goal: or (@IBet BTn A B x) (or (@eq (@ITpoint BTn) A B) (@eq (@ITpoint BTn) B x)) *)
tauto.
Qed.

Lemma eq_dec : forall A B :ITpoint, A=B \/ A<>B.
Proof.
(* Goal: forall A B : @ITpoint BTn, or (@eq (@ITpoint BTn) A B) (not (@eq (@ITpoint BTn) A B)) *)
intros.
(* Goal: or (@IBet BTn A B x) (or (@eq (@ITpoint BTn) A B) (@eq (@ITpoint BTn) B x)) *)
tauto.
Qed.

Definition BetT A B C := IBet A B C \/ A=B \/ B=C.

Lemma bet_id : forall A B : ITpoint, BetT A B A -> A = B.
Proof.
(* Goal: forall A B : @ITpoint BTn, or (@eq (@ITpoint BTn) A B) (not (@eq (@ITpoint BTn) A B)) *)
intros.
(* Goal: and (BetT P C B) (BetT Q C A) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
unfold BetT in H.
(* Goal: @eq (@ITpoint BTn) A B *)
decompose [or] H.
(* Goal: @eq (@ITpoint BTn) A B *)
apply Ibetween_identity in H0.
(* Goal: @eq (@ITpoint BTn) A B *)
elim H0.
(* Goal: not (@eq (@ITpoint BTn) A (@beeson_s_axioms.PA BTn)) *)
assumption.
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
intuition.
Qed.

Lemma IT_chara : forall A B C,
 IT A B C <-> A=B \/ B=C \/ IBet A B C.
Proof.
(* Goal: forall A B : @ITpoint BTn, or (@eq (@ITpoint BTn) A B) (not (@eq (@ITpoint BTn) A B)) *)
intros.
(* Goal: @IT BTn A B B *)
unfold IT.
(* Goal: or (@IBet BTn A B x) (or (@eq (@ITpoint BTn) A B) (@eq (@ITpoint BTn) B x)) *)
tauto. (* classical *)
Qed.

Lemma BetT_symmetry : forall A B C, BetT A B C -> BetT C B A.
Proof.
(* Goal: forall A B : @ITpoint BTn, or (@eq (@ITpoint BTn) A B) (not (@eq (@ITpoint BTn) A B)) *)
intros.
(* Goal: not (or (BetT (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn)) (or (BetT (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn)) (BetT (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn)))) *)
unfold BetT in *.
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
intuition.
(* Goal: or (@IBet BTn C Q B) (or (@eq (@ITpoint BTn) C Q) (@eq (@ITpoint BTn) Q B)) *)
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
left.
(* Goal: @IBet BTn C Q B *)
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
apply Ibetween_symmetry.
(* Goal: not (@eq (@ITpoint BTn) A (@beeson_s_axioms.PA BTn)) *)
assumption.
Qed.

Lemma BetT_id : forall A B, BetT A B A -> A=B.
Proof.
(* Goal: forall A B : @ITpoint BTn, or (@eq (@ITpoint BTn) A B) (not (@eq (@ITpoint BTn) A B)) *)
intros.
(* Goal: not (or (BetT (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn)) (or (BetT (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn)) (BetT (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn)))) *)
unfold BetT in *.
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
intuition.
(* Goal: @eq (@ITpoint BTn) A B *)
apply Ibetween_identity in H0.
(* Goal: @eq (@ITpoint BTn) A B *)
elim H0.
Qed.

(* Lemma 4.1 page 22 *)

Lemma pasch_col_case : forall A B C P Q : ITpoint,
        BetT A P C ->
        BetT B Q C -> ICol A B C -> exists x : ITpoint, BetT P x B /\ BetT Q x A.
Proof.
(* Goal: forall A B : @ITpoint BTn, or (@eq (@ITpoint BTn) A B) (not (@eq (@ITpoint BTn) A B)) *)
intros.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
elim (eq_dec A B);intro.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
 subst.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
 exists B.
(* Goal: BetT P B B *)
(* Goal: BetT Q B A *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
 unfold BetT;auto.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
elim (eq_dec A C);intro.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
 subst.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x C)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
 apply BetT_id in H.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
 subst.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn P x B) (or (@eq (@ITpoint BTn) P x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn C x A) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn P x B) (or (@eq (@ITpoint BTn) P x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn P x B) (or (@eq (@ITpoint BTn) P x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
 exists P.
(* Goal: BetT P B B *)
(* Goal: BetT Q B A *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
 unfold BetT;auto.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
elim (eq_dec B C);intro.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
 subst.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x C) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
 apply BetT_id in H0.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
 subst.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
 exists Q.
(* Goal: BetT P B B *)
(* Goal: BetT Q B A *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
 unfold BetT;auto.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
elim (eq_dec B Q);intro.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
 subst.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
 exists Q.
(* Goal: BetT P B B *)
(* Goal: BetT Q B A *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
 unfold BetT;auto.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
elim (eq_dec C Q);intro.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
 subst.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn P x B) (or (@eq (@ITpoint BTn) P x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn C x A) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn P x B) (or (@eq (@ITpoint BTn) P x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn P x B) (or (@eq (@ITpoint BTn) P x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
 exists P.
(* Goal: and (BetT B B x0) (@ICong BTn B x0 C D) *)
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
 split.
(* Goal: BetT P B B *)
(* Goal: BetT Q B A *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
 unfold BetT;auto.
(* Goal: BetT Q C A *)
(* Goal: and (BetT P C B) (BetT Q C A) *)
(* Goal: and (BetT P C B) (BetT Q C A) *)
(* Goal: and (BetT P C B) (BetT Q C A) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
 apply BetT_symmetry.
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
 auto.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
elim (eq_dec A P);intro.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
 subst.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn P x B) (or (@eq (@ITpoint BTn) P x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn C x A) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn P x B) (or (@eq (@ITpoint BTn) P x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn P x B) (or (@eq (@ITpoint BTn) P x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
 exists P.
(* Goal: BetT P B B *)
(* Goal: BetT Q B A *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
 unfold BetT;auto.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
elim (eq_dec C P);intro.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
 subst.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
 exists Q.
(* Goal: and (BetT B B x0) (@ICong BTn B x0 C D) *)
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
 split.
(* Goal: BetT Q C A *)
(* Goal: and (BetT P C B) (BetT Q C A) *)
(* Goal: and (BetT P C B) (BetT Q C A) *)
(* Goal: and (BetT P C B) (BetT Q C A) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
 apply BetT_symmetry.
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
 auto.
(* Goal: BetT P B B *)
(* Goal: BetT Q B A *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
 unfold BetT;auto.

(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
unfold ICol in H1.
(* Goal: and (BetT A B x) (@ICong BTn B x C D) *)
spliter.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply not_and_or in H1.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
induction H1.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply NNPP in H1.
(* Goal: not (or (or (@IBet BTn (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn)) (or (@eq (@ITpoint BTn) (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn)) (@eq (@ITpoint BTn) (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn)))) (or (or (@IBet BTn (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn)) (or (@eq (@ITpoint BTn) (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn)) (@eq (@ITpoint BTn) (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn)))) (or (@IBet BTn (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn)) (or (@eq (@ITpoint BTn) (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn)) (@eq (@ITpoint BTn) (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn)))))) *)
unfold IT in *.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply not_and_or in H1.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
induction H1.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply NNPP in H1.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
subst.
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
intuition.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply not_and_or in H1.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
induction H1.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply NNPP in H1.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
subst.
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
intuition.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply NNPP in H1.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
exists A.
(* Goal: and (BetT B B x0) (@ICong BTn B x0 C D) *)
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
split.
(* Goal: BetT P A B *)
(* Goal: BetT Q A A *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply Ibetween_symmetry in H1.
(* Goal: BetT P A B *)
(* Goal: BetT Q A A *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
induction H.
(* Goal: BetT P A B *)
(* Goal: BetT P A B *)
(* Goal: BetT Q A A *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
assert (T:=Ibetween_inner_transitivity B A P C H1 H).
(* Goal: BetT A B x *)
unfold BetT.
(* Goal: or (@IBet BTn C Q B) (or (@eq (@ITpoint BTn) C Q) (@eq (@ITpoint BTn) Q B)) *)
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
left.
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
apply Ibetween_symmetry;auto.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
induction H;subst.
(* Goal: BetT P B B *)
(* Goal: BetT Q B A *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
unfold BetT;auto.
(* Goal: or (@IBet BTn C Q B) (or (@eq (@ITpoint BTn) C Q) (@eq (@ITpoint BTn) Q B)) *)
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
left.
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
apply Ibetween_symmetry;auto.
(* Goal: BetT P B B *)
(* Goal: BetT Q B A *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
unfold BetT;auto.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply not_and_or in H1.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
induction H1.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply NNPP in H1.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
unfold IT in H1.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply not_and_or in H1.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
induction H1.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply NNPP in H1.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
subst.
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
intuition.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply not_and_or in H1.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
induction H1.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply NNPP in H1.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
subst.
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
intuition.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply NNPP in H1.

(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
exists C.

(* Goal: and (BetT P C B) (BetT Q C A) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
unfold BetT in H.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
induction H;induction H0.
(* Goal: and (BetT B B x0) (@ICong BTn B x0 C D) *)
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
split.
(* Goal: BetT Q C A *)
(* Goal: and (BetT P C B) (BetT Q C A) *)
(* Goal: and (BetT P C B) (BetT Q C A) *)
(* Goal: and (BetT P C B) (BetT Q C A) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply BetT_symmetry.
(* Goal: or (@IBet BTn C Q B) (or (@eq (@ITpoint BTn) C Q) (@eq (@ITpoint BTn) Q B)) *)
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
left.

(* Goal: @IBet BTn B C P *)
(* Goal: BetT Q C A *)
(* Goal: and (BetT P C B) (BetT Q C A) *)
(* Goal: and (BetT P C B) (BetT Q C A) *)
(* Goal: and (BetT P C B) (BetT Q C A) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply Ibetween_inner_transitivity with A.
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
apply Ibetween_symmetry;auto.
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
apply Ibetween_symmetry;auto.
(* Goal: BetT Q C A *)
(* Goal: and (BetT P C B) (BetT Q C A) *)
(* Goal: and (BetT P C B) (BetT Q C A) *)
(* Goal: and (BetT P C B) (BetT Q C A) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply BetT_symmetry.
(* Goal: or (@IBet BTn C Q B) (or (@eq (@ITpoint BTn) C Q) (@eq (@ITpoint BTn) Q B)) *)
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
left.
(* Goal: @IBet BTn A C Q *)
(* Goal: and (BetT P C B) (BetT Q C A) *)
(* Goal: and (BetT P C B) (BetT Q C A) *)
(* Goal: and (BetT P C B) (BetT Q C A) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply Ibetween_inner_transitivity with B.
(* Goal: not (@eq (@ITpoint BTn) A (@beeson_s_axioms.PA BTn)) *)
assumption.
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
apply Ibetween_symmetry;auto.
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
induction H0;subst;intuition.
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
induction H;subst;intuition.
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
induction H;subst;intuition.

(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply NNPP in H1.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
induction H;induction H0.

(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
exists B.
(* Goal: and (BetT B B x0) (@ICong BTn B x0 C D) *)
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
split.
(* Goal: BetT P B B *)
(* Goal: BetT Q B A *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
unfold BetT;auto.

(* Goal: or (@IBet BTn C Q B) (or (@eq (@ITpoint BTn) C Q) (@eq (@ITpoint BTn) Q B)) *)
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
left.
(* Goal: @IBet BTn C Q B *)
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
apply Ibetween_symmetry.
(* Goal: @IBet BTn A B Q *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply Ibetween_inner_transitivity with C.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
unfold IT in H1.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply not_and_or in H1.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
induction H1.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply NNPP in H1.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
subst.
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
intuition.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply not_and_or in H1.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
induction H1.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply NNPP in H1.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
subst.
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
intuition.
(* Goal: @IBet BTn A B C *)
(* Goal: @IBet BTn B Q C *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
apply NNPP in H1.
(* Goal: not (@eq (@ITpoint BTn) A (@beeson_s_axioms.PA BTn)) *)
assumption.
(* Goal: not (@eq (@ITpoint BTn) A (@beeson_s_axioms.PA BTn)) *)
assumption.

(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
induction H0;subst;intuition.
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
induction H;subst;intuition.
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
induction H;subst;intuition.
Qed.

Lemma pasch : forall A B C P Q : ITpoint,
        BetT A P C ->
        BetT B Q C -> exists x : ITpoint, BetT P x B /\ BetT Q x A.
Proof.
(* Goal: forall A B : @ITpoint BTn, or (@eq (@ITpoint BTn) A B) (not (@eq (@ITpoint BTn) A B)) *)
intros.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (BetT P x B) (BetT Q x A)) *)
induction (col_dec A B C).
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
eapply pasch_col_case;eauto.

(* Goal: not (or (BetT (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn)) (or (BetT (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn)) (BetT (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn)))) *)
unfold BetT in *.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn P x B) (or (@eq (@ITpoint BTn) P x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
decompose [or] H;clear H.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
decompose [or] H0;clear H0.

(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn P x B) (or (@eq (@ITpoint BTn) P x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn P x B) (or (@eq (@ITpoint BTn) P x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn P x B) (or (@eq (@ITpoint BTn) P x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn P x B) (or (@eq (@ITpoint BTn) P x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn P x B) (or (@eq (@ITpoint BTn) P x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
elim (Iinner_pasch A B C P Q H2 H H1).
(* Goal: forall A B : @ITpoint BTn, or (@eq (@ITpoint BTn) A B) (not (@eq (@ITpoint BTn) A B)) *)
intros.
(* Goal: and (BetT A B x) (@ICong BTn B x C D) *)
spliter.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
exists x.
(* Goal: and (BetT B B x0) (@ICong BTn B x0 C D) *)
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
split.
(* Goal: or (@IBet BTn A B x) (or (@eq (@ITpoint BTn) A B) (@eq (@ITpoint BTn) B x)) *)
tauto.
(* Goal: or (@IBet BTn A B x) (or (@eq (@ITpoint BTn) A B) (@eq (@ITpoint BTn) B x)) *)
tauto.

(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
subst.
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
exists Q;auto.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
subst.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn P x B) (or (@eq (@ITpoint BTn) P x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn C x A) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn P x B) (or (@eq (@ITpoint BTn) P x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn P x B) (or (@eq (@ITpoint BTn) P x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
exists P.
(* Goal: and (BetT B B x0) (@ICong BTn B x0 C D) *)
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
split.
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
auto.
(* Goal: or (@IBet BTn C Q B) (or (@eq (@ITpoint BTn) C Q) (@eq (@ITpoint BTn) Q B)) *)
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
left.
(* Goal: @IBet BTn C Q B *)
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
apply Ibetween_symmetry.
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
auto.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
subst.
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
exists P;auto.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
subst.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
decompose [or] H0;clear H0.
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
exists Q.
(* Goal: and (BetT B B x0) (@ICong BTn B x0 C D) *)
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
split.
(* Goal: or (@IBet BTn C Q B) (or (@eq (@ITpoint BTn) C Q) (@eq (@ITpoint BTn) Q B)) *)
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
left.
(* Goal: @IBet BTn C Q B *)
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
apply Ibetween_symmetry.
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
auto.
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
auto.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
subst.
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
exists Q;auto.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
subst.
(* Goal: or (@IBet BTn Q Q A) (or (@eq (@ITpoint BTn) Q Q) (@eq (@ITpoint BTn) Q A)) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
(* Goal: @ex (@ITpoint BTn) (fun x : @ITpoint BTn => and (or (@IBet BTn C x B) (or (@eq (@ITpoint BTn) C x) (@eq (@ITpoint BTn) x B))) (or (@IBet BTn Q x A) (or (@eq (@ITpoint BTn) Q x) (@eq (@ITpoint BTn) x A)))) *)
exists C;auto.
Qed.

Lemma five_segment:
 forall A A' B B' C C' D D' : ITpoint,
        ICong A B A' B' ->
        ICong B C B' C' ->
        ICong A D A' D' ->
        ICong B D B' D' ->
        BetT A B C -> BetT A' B' C' -> A <> B -> ICong C D C' D'.
Proof.
(* Goal: forall A B : @ITpoint BTn, or (@eq (@ITpoint BTn) A B) (not (@eq (@ITpoint BTn) A B)) *)
intros.
(* Goal: not (@eq (@ITpoint BTn) A (@beeson_s_axioms.PA BTn)) *)
apply Ifive_segment with A A' B B' ;try assumption.
(* Goal: @IT BTn A B B *)
unfold IT.
(* Goal: not (and (not (@eq (@ITpoint BTn) A B)) (and (not (@eq (@ITpoint BTn) B B)) (not (@IBet BTn A B B)))) *)
intro.
(* Goal: and (BetT A B x) (@ICong BTn B x C D) *)
spliter.
(* Goal: not (or (BetT (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn)) (or (BetT (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn)) (BetT (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn)))) *)
unfold BetT in *.
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
intuition.
(* Goal: not (or (BetT (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn)) (or (BetT (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn)) (BetT (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn)))) *)
unfold BetT in *.
(* Goal: @IT BTn A B B *)
unfold IT.
(* Goal: not (and (not (@eq (@ITpoint BTn) A B)) (and (not (@eq (@ITpoint BTn) B B)) (not (@IBet BTn A B B)))) *)
intro.
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
intuition.
Qed.

Lemma IT_trivial : forall A B, IT A A B.
Proof.
(* Goal: forall A B : @ITpoint BTn, or (@eq (@ITpoint BTn) A B) (not (@eq (@ITpoint BTn) A B)) *)
intros.
(* Goal: @IT BTn A B B *)
unfold IT.
(* Goal: not (and (not (@eq (@ITpoint BTn) A B)) (and (not (@eq (@ITpoint BTn) B B)) (not (@IBet BTn A B B)))) *)
intro.
(* Goal: and (BetT A B x) (@ICong BTn B x C D) *)
spliter.
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
intuition.
Qed.

Lemma IT_trivial2 : forall A B, IT A B B.
Proof.
(* Goal: forall A B : @ITpoint BTn, or (@eq (@ITpoint BTn) A B) (not (@eq (@ITpoint BTn) A B)) *)
intros.
(* Goal: @IT BTn A B B *)
unfold IT.
(* Goal: not (and (not (@eq (@ITpoint BTn) A B)) (and (not (@eq (@ITpoint BTn) B B)) (not (@IBet BTn A B B)))) *)
intro.
(* Goal: and (BetT A B x) (@ICong BTn B x C D) *)
spliter.
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
intuition.
Qed.

Lemma another_point : forall A, exists B:ITpoint, A<>B.
Proof.
(* Goal: forall A B : @ITpoint BTn, or (@eq (@ITpoint BTn) A B) (not (@eq (@ITpoint BTn) A B)) *)
intros.
(* Goal: not (or (BetT (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn)) (or (BetT (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn)) (BetT (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn)))) *)
assert (T:=Ilower_dim).
(* Goal: not (and (not (@eq (@ITpoint BTn) A B)) (and (not (@eq (@ITpoint BTn) B B)) (not (@IBet BTn A B B)))) *)
elim (eq_dec A beeson_s_axioms.PA);intro.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
subst.
(* Goal: not (and (not (@eq (@ITpoint BTn) A B)) (and (not (@eq (@ITpoint BTn) B B)) (not (@IBet BTn A B B)))) *)
elim (eq_dec beeson_s_axioms.PA beeson_s_axioms.PB);intro.
(* Goal: @ex (@ITpoint BTn) (fun B : @ITpoint BTn => not (@eq (@ITpoint BTn) (@beeson_s_axioms.PA BTn) B)) *)
(* Goal: @ex (@ITpoint BTn) (fun B : @ITpoint BTn => not (@eq (@ITpoint BTn) (@beeson_s_axioms.PA BTn) B)) *)
(* Goal: @ex (@ITpoint BTn) (fun B : @ITpoint BTn => not (@eq (@ITpoint BTn) A B)) *)
rewrite <- H in *.
(* Goal: @ex (@ITpoint BTn) (fun B : @ITpoint BTn => not (@eq (@ITpoint BTn) (@beeson_s_axioms.PA BTn) B)) *)
(* Goal: @ex (@ITpoint BTn) (fun B : @ITpoint BTn => not (@eq (@ITpoint BTn) (@beeson_s_axioms.PA BTn) B)) *)
(* Goal: @ex (@ITpoint BTn) (fun B : @ITpoint BTn => not (@eq (@ITpoint BTn) A B)) *)
exfalso.
(* Goal: False *)
(* Goal: @ex (@ITpoint BTn) (fun B : @ITpoint BTn => not (@eq (@ITpoint BTn) (@beeson_s_axioms.PA BTn) B)) *)
(* Goal: @ex (@ITpoint BTn) (fun B : @ITpoint BTn => not (@eq (@ITpoint BTn) A B)) *)
apply T.
(* Goal: @IT BTn (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PC BTn) *)
(* Goal: @ex (@ITpoint BTn) (fun B : @ITpoint BTn => not (@eq (@ITpoint BTn) (@beeson_s_axioms.PA BTn) B)) *)
(* Goal: @ex (@ITpoint BTn) (fun B : @ITpoint BTn => not (@eq (@ITpoint BTn) A B)) *)
apply IT_trivial.
(* Goal: @ex (@ITpoint BTn) (fun B : @ITpoint BTn => not (@eq (@ITpoint BTn) (@beeson_s_axioms.PA BTn) B)) *)
(* Goal: @ex (@ITpoint BTn) (fun B : @ITpoint BTn => not (@eq (@ITpoint BTn) A B)) *)
exists beeson_s_axioms.PB.
(* Goal: not (@eq (@ITpoint BTn) A (@beeson_s_axioms.PA BTn)) *)
assumption.
(* Goal: @ex (@ITpoint BTn) (fun B : @ITpoint BTn => not (@eq (@ITpoint BTn) A B)) *)
exists beeson_s_axioms.PA.
(* Goal: not (@eq (@ITpoint BTn) A (@beeson_s_axioms.PA BTn)) *)
assumption.
Qed.

Lemma segment_construction :
 forall A B C D : ITpoint,
        exists E : ITpoint, BetT A B E /\ ICong B E C D.
Proof.
(* Goal: forall A B : @ITpoint BTn, or (@eq (@ITpoint BTn) A B) (not (@eq (@ITpoint BTn) A B)) *)
intros.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
induction (eq_dec A B).
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
subst.
(* Goal: forall A B : @ITpoint BTn, or (@eq (@ITpoint BTn) A B) (not (@eq (@ITpoint BTn) A B)) *)
elim (another_point B);intros.
(* Goal: forall A B : @ITpoint BTn, or (@eq (@ITpoint BTn) A B) (not (@eq (@ITpoint BTn) A B)) *)
elim (Isegment_construction x B C D);intros.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT B B E) (@ICong BTn B E C D)) *)
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
exists x0.
(* Goal: and (BetT B B x0) (@ICong BTn B x0 C D) *)
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
split.
(* Goal: BetT A B x *)
unfold BetT.
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
intuition.
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
intuition.
(* Goal: not (@eq (@ITpoint BTn) x B) *)
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
intuition.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
elim (Isegment_construction A B C D H).
(* Goal: forall A B : @ITpoint BTn, or (@eq (@ITpoint BTn) A B) (not (@eq (@ITpoint BTn) A B)) *)
intros.
(* Goal: @ex (@ITpoint BTn) (fun E : @ITpoint BTn => and (BetT A B E) (@ICong BTn B E C D)) *)
exists x.
(* Goal: and (BetT A B x) (@ICong BTn B x C D) *)
spliter.
(* Goal: not (@eq (@ITpoint BTn) A (@beeson_s_axioms.PA BTn)) *)
split;try assumption.
(* Goal: not (or (or (@IBet BTn (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn)) (or (@eq (@ITpoint BTn) (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn)) (@eq (@ITpoint BTn) (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn)))) (or (or (@IBet BTn (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn)) (or (@eq (@ITpoint BTn) (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn)) (@eq (@ITpoint BTn) (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn)))) (or (@IBet BTn (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn)) (or (@eq (@ITpoint BTn) (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn)) (@eq (@ITpoint BTn) (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn)))))) *)
unfold IT in *.
(* Goal: BetT A B x *)
unfold BetT.
(* Goal: or (@IBet BTn A B x) (or (@eq (@ITpoint BTn) A B) (@eq (@ITpoint BTn) B x)) *)
tauto.
Qed.

Lemma lower_dim :
  ~ (BetT beeson_s_axioms.PA beeson_s_axioms.PB beeson_s_axioms.PC \/ 
     BetT beeson_s_axioms.PB beeson_s_axioms.PC beeson_s_axioms.PA \/ 
     BetT beeson_s_axioms.PC beeson_s_axioms.PA beeson_s_axioms.PB).
Proof.
(* Goal: not (or (BetT (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn)) (or (BetT (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn)) (BetT (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn)))) *)
assert (T:=Ilower_dim).
(* Goal: not (or (BetT (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn)) (or (BetT (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn)) (BetT (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn)))) *)
unfold BetT in *.
unfold ICol in  *.
(* Goal: not (or (or (@IBet BTn (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn)) (or (@eq (@ITpoint BTn) (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn)) (@eq (@ITpoint BTn) (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn)))) (or (or (@IBet BTn (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn)) (or (@eq (@ITpoint BTn) (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn)) (@eq (@ITpoint BTn) (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn)))) (or (@IBet BTn (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn)) (or (@eq (@ITpoint BTn) (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn)) (@eq (@ITpoint BTn) (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn)))))) *)
unfold IT in *.
(* Goal: not (or (or (@IBet BTn (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn)) (or (@eq (@ITpoint BTn) (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn)) (@eq (@ITpoint BTn) (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn)))) (or (or (@IBet BTn (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn)) (or (@eq (@ITpoint BTn) (@beeson_s_axioms.PB BTn) (@beeson_s_axioms.PC BTn)) (@eq (@ITpoint BTn) (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn)))) (or (@IBet BTn (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn)) (or (@eq (@ITpoint BTn) (@beeson_s_axioms.PC BTn) (@beeson_s_axioms.PA BTn)) (@eq (@ITpoint BTn) (@beeson_s_axioms.PA BTn) (@beeson_s_axioms.PB BTn)))))) *)
firstorder using Ibetween_symmetry.
Qed.

Lemma eq_dec_points_from_classic : forall A B : ITpoint, A = B \/ A <> B.
Proof.
(* Goal: forall A B : @ITpoint BTn, or (@eq (@ITpoint BTn) A B) (not (@eq (@ITpoint BTn) A B)) *)
intros.
(* Goal: or (@eq (@ITpoint BTn) A B) (not (@eq (@ITpoint BTn) A B)) *)
apply classic.
Qed.

Instance IT_to_T : Tarski_neutral_dimensionless.
exact
(Build_Tarski_neutral_dimensionless
   ITpoint BetT ICong
   Icong_pseudo_reflexivity Icong_inner_transitivity Icong_identity
   segment_construction five_segment
   bet_id pasch beeson_s_axioms.PA beeson_s_axioms.PB beeson_s_axioms.PC lower_dim).
Defined.

Instance IT_to_TID :
  Tarski_neutral_dimensionless_with_decidable_point_equality IT_to_T.
Proof. split; apply eq_dec_points_from_classic. Defined.

End Intuitionistic_Tarski_to_Tarski.