Require Export GeoCoq.Tarski_dev.Ch02_cong.

Section T2_1.

Context `{Tn:Tarski_neutral_dimensionless}.

Lemma bet_col : forall A B C, Bet A B C -> Col A B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Bet Tn A B C), @Col Tn A B C *)
    intros;unfold Col;auto.
Qed.

Lemma between_trivial : forall A B : Tpoint, Bet A B B.
Proof.
(* Goal: forall (A B C A' B' C' : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Bet Tn A' B' C') (_ : @Cong Tn A B A' B') (_ : @Cong Tn B C B' C'), @Cong Tn A C A' C' *)
    intros.
(* Goal: @Bet Tn A B B *)
    prolong A B x B B.
(* Goal: @Bet Tn A B B *)
    assert (x = B) by (apply cong_reverse_identity with B; Cong).
(* Goal: @Bet Tn A B B *)
    subst;assumption.
Qed.

Lemma between_symmetry : forall A B C : Tpoint, Bet A B C -> Bet C B A.
Proof.
(* Goal: forall (A B C A' B' C' : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Bet Tn A' B' C') (_ : @Cong Tn A B A' B') (_ : @Cong Tn B C B' C'), @Cong Tn A C A' C' *)
    intros.
(* Goal: @Bet Tn C B A *)
    assert (Bet B C C) by (apply between_trivial).
(* Goal: @Bet Tn C B A *)
    assert(exists x, Bet B x B /\ Bet C x A) by (apply inner_pasch with C;auto).
(* Goal: @Bet Tn A B C *)
    ex_and H1 x.
(* Goal: @Bet Tn C B A *)
    apply between_identity in H1; subst; assumption.
Qed.

(** This lemma is used by tactics for trying several permutations. *)
Lemma Bet_cases :
 forall A B C,
 Bet A B C \/ Bet C B A ->
 Bet A B C.
Proof.
(* Goal: forall (A B C A' B' C' : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Bet Tn A' B' C') (_ : @Cong Tn A B A' B') (_ : @Cong Tn B C B' C'), @Cong Tn A C A' C' *)
    intros.
(* Goal: @Bet Tn A B C *)
    decompose [or] H; auto using between_symmetry.
Qed.

Lemma Bet_perm :
  forall A B C,
 Bet A B C ->
 Bet A B C /\ Bet C B A.
Proof.
(* Goal: forall (A B C A' B' C' : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Bet Tn A' B' C') (_ : @Cong Tn A B A' B') (_ : @Cong Tn B C B' C'), @Cong Tn A C A' C' *)
    intros.
(* Goal: and (@Bet Tn A B C) (@Bet Tn C B A) *)
    auto using between_symmetry.
Qed.

Lemma between_trivial2 : forall A B : Tpoint, Bet A A B.
Proof.
(* Goal: forall (A B C A' B' C' : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Bet Tn A' B' C') (_ : @Cong Tn A B A' B') (_ : @Cong Tn B C B' C'), @Cong Tn A C A' C' *)
    intros.
(* Goal: @Bet Tn A B D *)
    apply between_symmetry.
(* Goal: @Bet Tn B B B *)
    apply between_trivial.
Qed.

Lemma between_equality : forall A B C : Tpoint, Bet A B C -> Bet B A C -> A = B.
Proof.
(* Goal: forall (A B C A' B' C' : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Bet Tn A' B' C') (_ : @Cong Tn A B A' B') (_ : @Cong Tn B C B' C'), @Cong Tn A C A' C' *)
    intros.
(* Goal: @eq (@Tpoint Tn) A B *)
    assert (exists x, Bet B x B /\ Bet A x A) by (apply (inner_pasch A B C);assumption).
(* Goal: @Bet Tn A B C *)
    ex_and H1 x.
(* Goal: @eq (@Tpoint Tn) A B *)
    apply between_identity in H1.
(* Goal: @eq (@Tpoint Tn) A B *)
    apply between_identity in H2.
(* Goal: @eq (@Tpoint Tn) A B *)
    congruence.
Qed.

Lemma between_equality_2 : forall A B C : Tpoint, Bet A B C -> Bet A C B -> B = C.
Proof.
(* Goal: forall (A B C A' B' C' : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Bet Tn A' B' C') (_ : @Cong Tn A B A' B') (_ : @Cong Tn B C B' C'), @Cong Tn A C A' C' *)
    intros.
(* Goal: and (@Bet Tn A B C) (@Bet Tn C B A) *)
    apply between_equality with A; auto using between_symmetry.
Qed.

Lemma between_exchange3 : forall A B C D, Bet A B C -> Bet A C D -> Bet B C D.
Proof.
(* Goal: forall (A B C A' B' C' : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Bet Tn A' B' C') (_ : @Cong Tn A B A' B') (_ : @Cong Tn B C B' C'), @Cong Tn A C A' C' *)
intros.
assert (exists x, Bet C x C /\ Bet B x D)
  by (apply inner_pasch with A; apply between_symmetry; auto).
(* Goal: @Bet Tn A B C *)
ex_and H1 x.
(* Goal: @Bet Tn B C D *)
assert (C = x) by (apply between_identity; auto); subst; auto.
Qed.

Lemma bet_neq12__neq : forall A B C, Bet A B C -> A <> B -> A <> C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : not (@eq (@Tpoint Tn) A B)), not (@eq (@Tpoint Tn) A C) *)
    intros A B C HBet HAB Heq.
(* Goal: False *)
    subst C; apply HAB, between_identity; trivial.
Qed.

Lemma bet_neq21__neq : forall A B C, Bet A B C -> B <> A -> A <> C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : not (@eq (@Tpoint Tn) C B)), not (@eq (@Tpoint Tn) A C) *)
    intros A B C HBet HAB.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
    apply bet_neq12__neq with B; auto.
Qed.

Lemma bet_neq23__neq : forall A B C, Bet A B C -> B <> C -> A <> C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : not (@eq (@Tpoint Tn) B C)), not (@eq (@Tpoint Tn) A C) *)
    intros A B C HBet HBC Heq.
(* Goal: False *)
    subst C; apply HBC; symmetry.
(* Goal: @eq (@Tpoint Tn) A B *)
    apply between_identity; trivial.
Qed.

Lemma bet_neq32__neq : forall A B C, Bet A B C -> C <> B -> A <> C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : not (@eq (@Tpoint Tn) C B)), not (@eq (@Tpoint Tn) A C) *)
    intros A B C HBet HAB.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
    apply bet_neq23__neq with B; auto.
Qed.

Lemma not_bet_distincts : forall A B C, ~ Bet A B C -> A <> B /\ B <> C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Bet Tn A B C)), and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C)) *)
    intros A B C HNBet.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) B C)) *)
    repeat split; intro; subst B; apply HNBet.
(* Goal: @Bet Tn A A C *)
(* Goal: @Bet Tn A C C *)
      apply between_trivial2.
(* Goal: @Bet Tn B B B *)
      apply between_trivial.
Qed.

End T2_1.

(** Some tactics *)

Ltac not_exist_hyp_perm_col A B C := not_exist_hyp (Col A B C); not_exist_hyp (Col A C B);
                                 not_exist_hyp (Col B A C); not_exist_hyp (Col B C A);
                                 not_exist_hyp (Col C A B); not_exist_hyp (Col C B A).

Ltac assert_cols :=
repeat
 match goal with
      | H:Bet ?X1 ?X2 ?X3 |- _ =>
     not_exist_hyp_perm_col X1 X2 X3;assert (Col X1 X2 X3) by (apply bet_col;apply H)
 end.

Ltac clean_trivial_hyps :=
  repeat
  match goal with
   | H:(Cong ?X1 ?X1 ?X2 ?X2) |- _ => clear H
   | H:(Cong ?X1 ?X2 ?X2 ?X1) |- _ => clear H
   | H:(Cong ?X1 ?X2 ?X1 ?X2) |- _ => clear H
   | H:(Bet ?X1 ?X1 ?X2) |- _ => clear H
   | H:(Bet ?X2 ?X1 ?X1) |- _ => clear H
   | H:(Col ?X1 ?X1 ?X2) |- _ => clear H
   | H:(Col ?X2 ?X1 ?X1) |- _ => clear H
   | H:(Col ?X1 ?X2 ?X1) |- _ => clear H
end.

Ltac clean_reap_hyps :=
  clean_duplicated_hyps;
  repeat
  match goal with
   | H:(Col ?A ?B ?C), H2 : Col ?A ?C ?B |- _ => clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?B ?A ?C |- _ => clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?B ?C ?A |- _ => clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?C ?B ?A |- _ => clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?C ?A ?B |- _ => clear H2
   | H:(Bet ?A ?B ?C), H2 : Bet ?C ?B ?A |- _ => clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?A ?B ?D ?C |- _ => clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?C ?D ?A ?B |- _ => clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?C ?D ?B ?A |- _ => clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?D ?C ?B ?A |- _ => clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?D ?C ?A ?B |- _ => clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?B ?A ?C ?D |- _ => clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?B ?A ?D ?C |- _ => clear H2
   | H:(?A<>?B), H2 : (?B<>?A) |- _ => clear H2
end.

Ltac clean := clean_trivial_hyps;clean_reap_hyps.

Ltac smart_subst X := subst X;clean.

Ltac treat_equalities_aux :=
  repeat
  match goal with
   | H:(?X1 = ?X2) |- _ => smart_subst X2
end.

Ltac treat_equalities :=
try treat_equalities_aux;
repeat
  match goal with
   | H:(Cong ?X3 ?X3 ?X1 ?X2) |- _ =>
      apply cong_symmetry in H; apply cong_identity in H;smart_subst X2
   | H:(Cong ?X1 ?X2 ?X3 ?X3) |- _ =>
      apply cong_identity in H;smart_subst X2
   | H:(Bet ?X1 ?X2 ?X1) |- _ => apply  between_identity in H;smart_subst X2
end.

Ltac show_distinct X Y := assert (X<>Y);[unfold not;intro;treat_equalities|idtac].

Hint Resolve between_symmetry bet_col : between.
Hint Resolve between_trivial between_trivial2 : between_no_eauto.

Ltac eBetween := treat_equalities;eauto with between.
Ltac Between := treat_equalities;auto with between between_no_eauto.

Section T2_2.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma between_inner_transitivity : forall A B C D, Bet A B D -> Bet B C D -> Bet A B C.
Proof.
(* Goal: forall (A B C A' B' C' : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Bet Tn A' B' C') (_ : @Cong Tn A B A' B') (_ : @Cong Tn B C B' C'), @Cong Tn A C A' C' *)
    intros.
(* Goal: @Bet Tn A B C *)
    assert (exists x, Bet B x B /\ Bet C x A) by (apply inner_pasch with D;auto).
(* Goal: @Bet Tn A B C *)
    ex_and H1 x.
(* Goal: @Bet Tn A B C *)
    Between.
Qed.

Lemma outer_transitivity_between2 : forall A B C D, Bet A B C -> Bet B C D -> B<>C -> Bet A C D.
Proof.
(* Goal: forall (A B C A' B' C' : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Bet Tn A' B' C') (_ : @Cong Tn A B A' B') (_ : @Cong Tn B C B' C'), @Cong Tn A C A' C' *)
    intros.
(* Goal: @Bet Tn A C D *)
    prolong A C x C D.
(* Goal: @Bet Tn A C D *)
    assert (x = D) by (apply (construction_uniqueness B C C D); try apply (between_exchange3 A B C x); Cong).
(* Goal: @Bet Tn A C D *)
    subst x;assumption.
Qed.

End T2_2.

Hint Resolve outer_transitivity_between2 between_inner_transitivity between_exchange3 : between.

Section T2_3.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma between_exchange2 : forall A B C D, Bet A B D -> Bet B C D -> Bet A C D.
Proof.
(* Goal: forall (A B C A' B' C' : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Bet Tn A' B' C') (_ : @Cong Tn A B A' B') (_ : @Cong Tn B C B' C'), @Cong Tn A C A' C' *)
    intros.
(* Goal: @Bet Tn A B C *)
    induction (eq_dec_points B C);eBetween.
Qed.

Lemma outer_transitivity_between : forall A B C D, Bet A B C -> Bet B C D -> B<>C -> Bet A B D.
Proof.
(* Goal: forall (A B C A' B' C' : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Bet Tn A' B' C') (_ : @Cong Tn A B A' B') (_ : @Cong Tn B C B' C'), @Cong Tn A C A' C' *)
    intros.
(* Goal: @Bet Tn A B D *)
    apply between_symmetry.
(* Goal: @Bet Tn A B C *)
    apply (outer_transitivity_between2) with C; Between.
Qed.

Lemma between_exchange4 : forall A B C D, Bet A B C -> Bet A C D -> Bet A B D.
Proof.
(* Goal: forall (A B C A' B' C' : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Bet Tn A' B' C') (_ : @Cong Tn A B A' B') (_ : @Cong Tn B C B' C'), @Cong Tn A C A' C' *)
    intros.
(* Goal: @Bet Tn A B D *)
    apply between_symmetry.
(* Goal: @Bet Tn A B C *)
    apply between_exchange2 with C; Between.
Qed.

End T2_3.

Hint Resolve between_exchange2 outer_transitivity_between between_exchange4 : between.

Section T2_4.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma l3_9_4 : forall A1 A2 A3 A4, Bet_4 A1 A2 A3 A4 -> Bet_4 A4 A3 A2 A1.
Proof.
(* Goal: forall (A1 A2 A3 A4 : @Tpoint Tn) (_ : @Bet_4 Tn A1 A2 A3 A4), @Bet_4 Tn A4 A3 A2 A1 *)
    unfold Bet_4.
(* Goal: forall (A1 A2 A3 A4 : @Tpoint Tn) (_ : and (@Bet Tn A1 A2 A3) (and (@Bet Tn A2 A3 A4) (and (@Bet Tn A1 A3 A4) (@Bet Tn A1 A2 A4)))), and (@Bet Tn A4 A3 A2) (and (@Bet Tn A3 A2 A1) (and (@Bet Tn A4 A2 A1) (@Bet Tn A4 A3 A1))) *)
    intros;spliter; auto with between.
Qed.

Lemma l3_17 : forall A B C A' B' P,
  Bet A B C -> Bet A' B' C -> Bet A P A' -> exists Q, Bet P Q C /\ Bet B Q B'.
Proof.
(* Goal: forall (A B C A' B' C' : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Bet Tn A' B' C') (_ : @Cong Tn A B A' B') (_ : @Cong Tn B C B' C'), @Cong Tn A C A' C' *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Bet Tn P Q C) (@Bet Tn B Q B')) *)
    assert (exists Q', Bet B' Q' A /\ Bet P Q' C) by (eapply inner_pasch;eBetween).
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Bet Tn P Q C) (@Bet Tn B Q B')) *)
    ex_and H2 x.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Bet Tn P Q C) (@Bet Tn B Q B')) *)
    assert (exists y, Bet x y C /\ Bet B y B') by (eapply inner_pasch;eBetween).
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Bet Tn P Q C) (@Bet Tn B Q B')) *)
    ex_and H4 y.
(* Goal: @Bet Tn A B C *)
    exists y;eBetween.
Qed.

(** The prove the former version of lower dimension axiom for compatibility. *)

Lemma lower_dim_ex : exists A B C,
  ~ (Bet A B C \/ Bet B C A \/ Bet C A B).
Proof.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (or (@Bet Tn A B C) (or (@Bet Tn B C A) (@Bet Tn C A B)))))) *)
exists PA.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (or (@Bet Tn (@PA Tn) B C) (or (@Bet Tn B C (@PA Tn)) (@Bet Tn C (@PA Tn) B))))) *)
exists PB.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (or (@Bet Tn (@PA Tn) (@PB Tn) C) (or (@Bet Tn (@PB Tn) C (@PA Tn)) (@Bet Tn C (@PA Tn) (@PB Tn))))) *)
exists PC.
(* Goal: not (or (@Bet Tn (@PA Tn) (@PB Tn) (@PC Tn)) (or (@Bet Tn (@PB Tn) (@PC Tn) (@PA Tn)) (@Bet Tn (@PC Tn) (@PA Tn) (@PB Tn)))) *)
apply lower_dim.
Qed.

Lemma two_distinct_points : exists X, exists Y: Tpoint, X <> Y.
Proof.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => not (@eq (@Tpoint Tn) X Y))) *)
    assert (ld:=lower_dim_ex).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => not (@eq (@Tpoint Tn) X Y))) *)
    ex_elim ld A.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => not (@eq (@Tpoint Tn) X Y))) *)
    ex_elim H B.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => not (@eq (@Tpoint Tn) X Y))) *)
    ex_elim H0 C.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => not (@eq (@Tpoint Tn) X Y))) *)
    exists A; exists B.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    intro; subst; apply H.
(* Goal: @Bet Tn B B B *)
    right; right; apply between_trivial.
Qed.

Lemma point_construction_different : forall A B, exists C, Bet A B C /\ B <> C.
Proof.
(* Goal: forall (A B C A' B' C' : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Bet Tn A' B' C') (_ : @Cong Tn A B A' B') (_ : @Cong Tn B C B' C'), @Cong Tn A C A' C' *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Bet Tn A B C) (not (@eq (@Tpoint Tn) B C))) *)
    assert (tdp := two_distinct_points).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Bet Tn A B C) (not (@eq (@Tpoint Tn) B C))) *)
    ex_elim tdp x.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Bet Tn A B C) (not (@eq (@Tpoint Tn) B C))) *)
    ex_elim H y.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Bet Tn A B C) (not (@eq (@Tpoint Tn) B C))) *)
    prolong A B F x y.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Bet Tn A B C) (not (@eq (@Tpoint Tn) B C))) *)
    exists F.
(* Goal: and (@Bet Tn A B F) (not (@eq (@Tpoint Tn) B F)) *)
    show_distinct B F.
(* Goal: and (@Bet Tn A B F) (not (@eq (@Tpoint Tn) B F)) *)
      intuition.
(* Goal: and (@Bet Tn A B F) (not (@eq (@Tpoint Tn) B F)) *)
    intuition.
Qed.

Lemma another_point : forall A: Tpoint, exists B, A<>B.
Proof.
(* Goal: forall (A B C A' B' C' : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Bet Tn A' B' C') (_ : @Cong Tn A B A' B') (_ : @Cong Tn B C B' C'), @Cong Tn A C A' C' *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => not (@eq (@Tpoint Tn) A B)) *)
    assert (pcd := point_construction_different A A).
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => not (@eq (@Tpoint Tn) A B)) *)
    ex_and pcd B.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => not (@eq (@Tpoint Tn) A B)) *)
    exists B;assumption.
Qed.

End T2_4.

Section Beeson_1.

(** Another proof of l2_11 without eq_dec_points but using Cong stability
inspired by Micheal Beeson. #<a href="http://www.michaelbeeson.com/research/papers/AxiomatizingConstructiveGeometry.pdf"></a> # *)

Context `{Tn:Tarski_neutral_dimensionless}.

Variable Cong_stability : forall A B C D, ~ ~ Cong A B C D -> Cong A B C D.

Lemma l2_11_b : forall A B C A' B' C',
 Bet A B C -> Bet A' B' C' -> Cong A B A' B' -> Cong B C B' C' -> Cong A C A' C'.
Proof.
(* Goal: forall (A B C A' B' C' : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Bet Tn A' B' C') (_ : @Cong Tn A B A' B') (_ : @Cong Tn B C B' C'), @Cong Tn A C A' C' *)
    intros.
(* Goal: @Cong Tn A C A' C' *)
    apply Cong_stability; intro.
(* Goal: False *)
    assert (A<>B).
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: False *)
      intro; subst.
(* Goal: False *)
(* Goal: False *)
      assert (A'=B') by (apply (cong_identity A' B' B); Cong).
(* Goal: False *)
(* Goal: False *)
      subst; tauto.
(* Goal: False *)
    assert (Cong C A C' A') by (apply (five_segment _ _ _ _ _ _ _ _ H1 );auto using cong_trivial_identity, cong_commutativity).
(* Goal: False *)
    apply H3; Cong.
Qed.

Lemma cong_dec_eq_dec_b :
 (forall A B:Tpoint, ~ A <> B -> A = B).
Proof.
(* Goal: forall (A B : @Tpoint Tn) (_ : not (not (@eq (@Tpoint Tn) A B))), @eq (@Tpoint Tn) A B *)
    intros A B HAB.
(* Goal: @eq (@Tpoint Tn) A B *)
    apply cong_identity with A.
(* Goal: @Cong Tn A B A A *)
    apply Cong_stability.
(* Goal: not (not (@Cong Tn A B A A)) *)
    intro HNCong.
(* Goal: False *)
    apply HAB.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    intro HEq.
(* Goal: False *)
    subst.
(* Goal: False *)
    apply HNCong.
(* Goal: @Cong Tn B B B B *)
    apply cong_pseudo_reflexivity.
Qed.

End Beeson_1.

Section Beeson_2.

Context `{Tn:Tarski_neutral_dimensionless}.

Variable Bet_stability : forall A B C, ~ ~ Bet A B C -> Bet A B C.

Lemma bet_dec_eq_dec_b :
 (forall A B:Tpoint, ~ A <> B -> A = B).
Proof.
(* Goal: forall (A B : @Tpoint Tn) (_ : not (not (@eq (@Tpoint Tn) A B))), @eq (@Tpoint Tn) A B *)
    intros A B HAB.
(* Goal: @eq (@Tpoint Tn) A B *)
    apply between_identity.
(* Goal: @Bet Tn A B A *)
    apply Bet_stability.
(* Goal: not (not (@Bet Tn A B A)) *)
    intro HNBet.
(* Goal: False *)
    apply HAB.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    intro HEq.
(* Goal: False *)
    subst.
(* Goal: False *)
    apply HNBet.
(* Goal: @Bet Tn B B B *)
    apply between_trivial.
Qed.

Lemma BetSEq : forall A B C, BetS A B C <-> Bet A B C /\ A <> B /\ A <> C /\ B <> C.
Proof.
intros; unfold BetS; split; intro; spliter;
repeat split; auto; intro; treat_equalities; auto.
Qed.

End Beeson_2.