Require Export GeoCoq.Tarski_dev.Ch04_col.
Require Import GeoCoq.Utils.all_equiv.

Section Equivalence_between_decidability_properties_of_basic_relations.

Context `{Tn:Tarski_neutral_dimensionless}.

Lemma cong_dec_eq_dec :
  (forall A B C D, Cong A B C D \/ ~ Cong A B C D) ->
  (forall A B:Tpoint, A=B \/ A<>B).
Proof.
(* Goal: forall (_ : forall A B C D : @Tpoint Tn, or (@Cong Tn A B C D) (not (@Cong Tn A B C D))) (A B : @Tpoint Tn), or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B)) *)
    intros H A B.
(* Goal: or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B)) *)
    elim (H A B A A); intro HCong.
(* Goal: or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B)) *)
(* Goal: or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B)) *)
      left; apply cong_identity with A; assumption.
(* Goal: or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B)) *)
    right; intro; subst; apply HCong.
(* Goal: @Cong Tn B B B B *)
    apply cong_pseudo_reflexivity.
Qed.

Lemma eq_dec_implies_l2_11 :
  (forall A B:Tpoint, A=B \/ A<>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 (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C : @Tpoint Tn), or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
intro eq_dec; intros.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => not (@eq (@Tpoint Tn) X Y))) *)
induction (eq_dec A B).
(* Goal: @Cong Tn A C A' C' *)
(* Goal: @Cong Tn A C A' C' *)
subst B.
(* Goal: @Cong Tn A C A' C' *)
(* Goal: @Cong Tn A C A' C' *)
assert (A' = B') by (apply (cong_identity A' B' A); Cong).
(* Goal: @Cong Tn A C A' C' *)
(* Goal: @Cong Tn A C A' C' *)
subst; Cong.
(* Goal: @Cong Tn A C A' C' *)
apply cong_commutativity; apply (five_segment A A' B B' C C' A A'); Cong.
Qed.

Lemma eq_dec_implies_construction_uniqueness :
  (forall A B:Tpoint, A=B \/ A<>B) ->
  forall Q A B C X Y,
  Q <> A -> Bet Q A X -> Cong A X B C -> Bet Q A Y -> Cong A Y B C -> X=Y.
Proof.
(* Goal: forall (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C : @Tpoint Tn), or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
intro eq_dec; intros.
(* Goal: @eq (@Tpoint Tn) X Y *)
assert (Cong A X A Y) by eCong.
(* Goal: @eq (@Tpoint Tn) X Y *)
assert (Cong Q X Q Y) by (apply (eq_dec_implies_l2_11 eq_dec Q A X Q A Y);Cong).
(* Goal: @eq (@Tpoint Tn) X Y *)
assert(OFSC Q A X Y Q A X X) by (unfold OFSC;repeat split;Cong).
(* Goal: @eq (@Tpoint Tn) X Y *)
apply five_segment_with_def in H6; try assumption.
(* Goal: @eq (@Tpoint Tn) X Y *)
apply cong_identity with X; Cong.
Qed.

Lemma eq_dec_implies_outer_transitivity_between2 :
  (forall A B:Tpoint, A=B \/ A<>B) ->
  forall A B C D, Bet A B C -> Bet B C D -> B<>C -> Bet A C D.
Proof.
(* Goal: forall (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C : @Tpoint Tn), or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
intro eq_dec; intros.
(* Goal: @Bet Tn A C D *)
prolong A C x C D.
(* Goal: @Bet Tn A C D *)
assert (x = D) by (apply (eq_dec_implies_construction_uniqueness eq_dec B C C D); try apply (between_exchange3 A B C x); Cong).
(* Goal: @Bet Tn A C D *)
subst x;assumption.
Qed.

Lemma eq_dec_implies_between_exchange4 :
  (forall A B:Tpoint, A=B \/ A<>B) ->
  forall A B C D, Bet A B C -> Bet A C D -> Bet A B D.
Proof.
(* Goal: forall (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C : @Tpoint Tn), or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
intro eq_dec; intros.
(* Goal: @Bet Tn A B D *)
induction (eq_dec B C); [subst; auto|].
apply between_symmetry;
apply eq_dec_implies_outer_transitivity_between2 with C; eBetween.
Qed.

Lemma eq_dec_implies_two_distinct_points :
  (forall A B:Tpoint, A=B \/ A<>B) ->
  exists X, exists Y: Tpoint, X <> Y.
Proof.
(* Goal: forall _ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B)), @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => not (@eq (@Tpoint Tn) X Y))) *)
intro eq_dec.
(* 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))) *)
induction (eq_dec A B).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => not (@eq (@Tpoint Tn) X Y))) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => not (@eq (@Tpoint Tn) X Y))) *)
subst A; exists B; exists C; Between.
(* 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; assumption.
Qed.

Lemma eq_dec_implies_point_construction_different :
  (forall A B:Tpoint, A=B \/ A<>B) ->
  forall A B, exists C, Bet A B C /\ B <> C.
Proof.
(* Goal: forall (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C : @Tpoint Tn), or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
intro eq_dec; intros.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Bet Tn A B C) (not (@eq (@Tpoint Tn) B C))) *)
assert (tdp := eq_dec_implies_two_distinct_points eq_dec).
(* 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: not (@eq (@Tpoint Tn) B A) *)
intuition.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
intuition.
Qed.

Lemma eq_dec_implies_l4_2 :
  (forall A B:Tpoint, A=B \/ A<>B) ->
  forall A B C D A' B' C' D', IFSC A B C D A' B' C' D' -> Cong B D B' D'.
Proof.
(* Goal: forall (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C D A' B' C' D' : @Tpoint Tn) (_ : @IFSC Tn A B C D A' B' C' D'), @Cong Tn B D B' D' *)
unfold IFSC.
(* Goal: forall (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C : @Tpoint Tn), or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
intro eq_dec; intros.
(* Goal: or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
spliter.

(* Goal: @Cong Tn B D B' D' *)
induction (eq_dec A C).

(* Goal: @Cong Tn B D B' D' *)
(* Goal: @Cong Tn B D B' D' *)
treat_equalities;assumption.

assert (exists E, Bet A C E /\ C <> E)
 by (apply eq_dec_implies_point_construction_different; auto).
(* Goal: @Cong Tn B D B' D' *)
ex_and H6 E.
(* Goal: @Cong Tn B D B' D' *)
prolong A' C' E' C E.

assert  (Cong E D E' D')
 by (
  apply (five_segment_with_def A C E D A' C' E' D');[
  unfold OFSC;  repeat split;Cong|
  assumption]).

(* Goal: @Cong Tn B D B' D' *)
apply (five_segment_with_def E C B D E' C' B' D').
(* Goal: @OFSC Tn E C B D E' C' B' D' *)
(* Goal: not (@eq (@Tpoint Tn) E C) *)
unfold OFSC.
(* Goal: and (@Bet Tn E C B) (and (@Bet Tn E' C' B') (and (@Cong Tn E C E' C') (and (@Cong Tn C B C' B') (and (@Cong Tn E D E' D') (@Cong Tn C D C' D'))))) *)
(* Goal: not (@eq (@Tpoint Tn) E C) *)
repeat split; try solve [eBetween| Cong ].
(* Goal: not (@eq (@Tpoint Tn) E C) *)
auto.
Qed.

Lemma eq_dec_implies_l4_5 :
  (forall A B:Tpoint, A=B \/ A<>B) ->
  forall A B C A' C',
  Bet A B C -> Cong A C A' C' ->
  exists B', Bet A' B' C' /\ Cong_3 A B C A' B' C'.
Proof.
(* Goal: forall (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C : @Tpoint Tn), or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
intro eq_dec; intros.
(* Goal: forall (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C A' B' C' : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Cong_3 Tn A B C A' B' C'), @Bet Tn A' B' C' *)
unfold Cong_3.

assert (exists D', Bet C' A' D' /\ A' <> D')
 by (apply eq_dec_implies_point_construction_different; auto).
ex_and H1 x'.
prolong x' A' B' A B.
prolong x' B' C'' B C.

assert (Bet A' B' C'') by eBetween.

assert (C'' = C').
eapply (eq_dec_implies_construction_uniqueness eq_dec x' A' ).

(* Goal: not (@eq (@Tpoint Tn) E C) *)
auto.

(* Goal: not (@eq (@Tpoint Tn) E C) *)
apply eq_dec_implies_between_exchange4 with B'; auto.

apply (eq_dec_implies_l2_11 eq_dec A' B' C'' A B C);Between.

eBetween.
Cong.

subst C''.
exists B'.
repeat split;Cong.
Qed.

Lemma eq_dec_implies_l4_6 :
  (forall A B:Tpoint, A=B \/ A<>B) ->
  forall A B C A' B' C', Bet A B C -> Cong_3 A B C A' B' C' -> Bet A' B' C'.
Proof.
(* Goal: forall (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C A' B' C' : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Cong_3 Tn A B C A' B' C'), @Bet Tn A' B' C' *)
unfold Cong_3.
(* Goal: forall (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C : @Tpoint Tn), or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
intro eq_dec; intros.
assert (exists B'', Bet A' B'' C' /\ Cong_3 A B C A' B'' C')
  by (eapply eq_dec_implies_l4_5;intuition).
(* Goal: @Bet Tn A' B' C' *)
ex_and H1 x.
(* Goal: or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
unfold Cong_3 in *;spliter.

assert (Cong_3 A' x C' A' B' C')
 by (unfold Cong_3;repeat split;eCong).
(* Goal: or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
unfold Cong_3 in H7;spliter.

assert (IFSC A' x C' x  A' x C' B')
 by (unfold IFSC;repeat split;Cong).
assert (Cong x x x B')
 by (eapply eq_dec_implies_l4_2; try apply H10; auto).
(* Goal: @Bet Tn A' B' C' *)
Between.
Qed.

Lemma eq_dec_implies_l4_16 :
  (forall A B:Tpoint, A=B \/ A<>B) ->
  forall A B C D A' B' C' D',
  FSC A B C D A' B' C' D' -> A<>B -> Cong C D C' D'.
Proof.
(* Goal: forall (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C D A' B' C' D' : @Tpoint Tn) (_ : @FSC Tn A B C D A' B' C' D') (_ : not (@eq (@Tpoint Tn) A B)), @Cong Tn C D C' D' *)
unfold FSC.
(* Goal: forall (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C D A' B' C' D' : @Tpoint Tn) (_ : and (@Col Tn A B C) (and (@Cong_3 Tn A B C A' B' C') (and (@Cong Tn A D A' D') (@Cong Tn B D B' D')))) (_ : not (@eq (@Tpoint Tn) A B)), @Cong Tn C D C' D' *)
unfold Col.
(* Goal: forall (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C : @Tpoint Tn), or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
intro eq_dec; intros.
(* Goal: @Cong Tn C D C' D' *)
decompose [or and] H; clear H.
(* Goal: @Cong Tn C D C' D' *)
(* Goal: @Cong Tn C D C' D' *)
(* Goal: @Cong Tn C D C' D' *)
assert (Bet A' B' C') by (eapply eq_dec_implies_l4_6;eauto).
(* Goal: or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
unfold Cong_3 in *; spliter.
(* Goal: @Cong Tn C D C' D' *)
(* Goal: @Cong Tn C D C' D' *)
(* Goal: @Cong Tn C D C' D' *)
assert(OFSC A B C D A' B' C' D') by (unfold OFSC;repeat split; assumption).
(* Goal: not (@eq (@Tpoint Tn) E C) *)
eapply five_segment_with_def; eauto.
(* Goal: @Cong Tn C D C' D' *)
(* Goal: @Cong Tn C D C' D' *)
assert(Bet B' C' A') by (apply (eq_dec_implies_l4_6 eq_dec B C A B' C' A'); Cong;auto with cong3).
(* Goal: @Cong Tn C D C' D' *)
(* Goal: @Cong Tn C D C' D' *)
apply (eq_dec_implies_l4_2 eq_dec B C A D B' C' A' D').
unfold IFSC; unfold Cong_3 in *; spliter; repeat split;Between;Cong.
(* Goal: @Cong Tn C D C' D' *)
assert (Bet C' A' B') by (eapply (eq_dec_implies_l4_6 eq_dec C A B C' A' B'); auto with cong3).
eapply (five_segment_with_def B A C D B' A'); unfold OFSC; unfold Cong_3 in *; spliter; repeat split; Between; Cong.
Qed.

Lemma eq_dec_implies_l4_17 :
  (forall A B:Tpoint, A=B \/ A<>B) ->
  forall A B C P Q,
  A<>B -> Col A B C -> Cong A P A Q -> Cong B P B Q -> Cong C P C Q.
Proof.
(* Goal: forall (x y : Prop) (_ : or (@eq Prop decidability_of_equality_of_points x) (or (@eq Prop decidability_of_congruence_of_points x) (or (@eq Prop decidability_of_betweenness_of_points x) False))) (_ : or (@eq Prop decidability_of_equality_of_points y) (or (@eq Prop decidability_of_congruence_of_points y) (or (@eq Prop decidability_of_betweenness_of_points y) False))), iff x y *)
intros.
(* Goal: @Cong Tn C P C Q *)
assert (FSC A B C P A B C Q) by (unfold FSC; unfold Cong_3; repeat split;Cong).
(* Goal: not (@eq (@Tpoint Tn) E C) *)
eapply eq_dec_implies_l4_16; eauto.
Qed.

Lemma eq_dec_implies_l5_1 :
  (forall A B:Tpoint, A=B \/ A<>B) ->
  forall A B C D,
  A<>B -> Bet A B C -> Bet A B D -> Bet A C D \/ Bet A D C.
Proof.
(* Goal: forall (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C : @Tpoint Tn), or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
intro eq_dec; intros.
prolong A D C' C D.
prolong A C D' C D.
prolong A C' B' C B.
prolong A D' B'' D B.
assert (Cong B C' B'' C).
apply (eq_dec_implies_l2_11 eq_dec B D C' B'' D' C).
(* Goal: @Bet Tn A' B' C' *)
apply between_exchange3 with A; Between.
(* Goal: @Bet Tn A' B' C' *)
apply between_inner_transitivity with A; Between.
Cong.
apply cong_transitivity with C D; Cong.
assert (Cong B B' B'' B).
  {
  apply (eq_dec_implies_l2_11 eq_dec B C' B' B'' C B); Cong.

    {
    assert (Bet A B C'); [|eBetween].
    induction (eq_dec B D); [treat_equalities; auto|].
    apply between_symmetry.
    apply eq_dec_implies_outer_transitivity_between2 with D; eBetween.
    }

    {
    induction (eq_dec C D'); [treat_equalities; eBetween|].
    apply eq_dec_implies_outer_transitivity_between2 with D'; eBetween.
    }
  }
assert(B'' =  B').
apply (eq_dec_implies_construction_uniqueness eq_dec A B B B''); try Cong.
apply eq_dec_implies_between_exchange4 with D'; Between;
(* Goal: @Bet Tn A' B' C' *)
apply eq_dec_implies_between_exchange4 with C; Between.
apply eq_dec_implies_between_exchange4 with C'; Between;
(* Goal: @Bet Tn A' B' C' *)
apply eq_dec_implies_between_exchange4 with D; Between.
subst B''.
assert (FSC B C D' C' B' C' D C).
(* Goal: forall (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C D A' B' C' D' : @Tpoint Tn) (_ : @FSC Tn A B C D A' B' C' D') (_ : not (@eq (@Tpoint Tn) A B)), @Cong Tn C D C' D' *)
unfold FSC.
repeat split; unfold Col; try Cong.
(* Goal: @Bet Tn A' B' C' *)
left; apply between_exchange3 with A; Between.
apply (eq_dec_implies_l2_11 eq_dec B C D' B' C' D); Cong.
apply between_exchange3 with A; assumption.
apply between_symmetry.
apply between_exchange3 with A; assumption.
apply cong_transitivity with C D; Cong.
apply cong_transitivity with C D; Cong.
induction (eq_dec B C).
(* Goal: not (@eq (@Tpoint Tn) E C) *)
subst C; auto.
assert (Cong D' C' D C) by (eapply eq_dec_implies_l4_16; try apply H12; assumption).
assert (exists E, Bet C E C' /\ Bet D E D') by (apply inner_pasch with A; Between).
ex_and H15 E.
assert (IFSC D E D' C D E D' C') by (unfold IFSC; repeat split; Cong; apply cong_transitivity with C D; Cong).
assert (IFSC C E C' D C E C' D') by (unfold IFSC; repeat split; Cong; apply cong_transitivity with C D; Cong).
assert (Cong E C E C') by (eapply eq_dec_implies_l4_2; try apply H17; auto).
assert (Cong E D E D') by (eapply eq_dec_implies_l4_2; try apply H18; auto).
induction (eq_dec C C').
subst C'; right; assumption.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
show_distinct C D'; intuition.
prolong C' C P C D'.
prolong D' C R C E.
prolong P R Q R P.
assert (FSC D' C R P P C E D').
(* Goal: forall (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C D A' B' C' D' : @Tpoint Tn) (_ : @FSC Tn A B C D A' B' C' D') (_ : not (@eq (@Tpoint Tn) A B)), @Cong Tn C D C' D' *)
unfold FSC.
(* Goal: forall (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C A' B' C' : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Cong_3 Tn A B C A' B' C'), @Bet Tn A' B' C' *)
unfold Cong_3.
assert_cols.
repeat split; Cong.
apply eq_dec_implies_l2_11 with C C; Cong.
(* Goal: @Bet Tn A' B' C' *)
apply between_inner_transitivity with C'; Between.
assert (Cong R P E D') by (eauto using eq_dec_implies_l4_16).
assert (Cong R Q E D).
eapply cong_transitivity.
apply cong_transitivity with R P; Cong.
apply cong_transitivity with E D'; Cong.
assert (FSC D' E D C P R Q C).
(* Goal: forall (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C D A' B' C' D' : @Tpoint Tn) (_ : @FSC Tn A B C D A' B' C' D') (_ : not (@eq (@Tpoint Tn) A B)), @Cong Tn C D C' D' *)
unfold FSC.
repeat split; Cong.
(* Goal: @Bet Tn A' B' C' *)
unfold Col; Between.
eapply (eq_dec_implies_l2_11 eq_dec D' E D P R Q); Between; Cong.
assert (Cong D C Q C).
induction (eq_dec D' E).
unfold FSC, IFSC, Cong_3 in *; spliter; treat_equalities; Cong.
apply eq_dec_implies_l4_16 with D' E P R; assumption.
assert (Cong C P C Q).
unfold FSC in *;unfold Cong_3 in *.
(* Goal: or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
spliter.
apply cong_transitivity with C D.
apply cong_transitivity with C D'; Cong.
Cong.
show_distinct R C.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
intuition.
assert (Cong D' P D' Q) by (apply (eq_dec_implies_l4_17 eq_dec R C); unfold Col; Between; Cong).
assert (Cong B P B Q).
apply eq_dec_implies_l4_17 with C D'; try assumption.
unfold Col; right;right.
apply between_exchange3 with A; assumption.
assert (Cong B' P B' Q).
eapply (eq_dec_implies_l4_17 eq_dec C D'); Cong.
unfold Col; left.
apply between_exchange3 with A; assumption.
assert (Cong C' P C' Q).
induction(eq_dec B B').
subst B'.
unfold IFSC,FSC, Cong_3 in *.
(* Goal: or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
spliter.
clean_duplicated_hyps.
clean_trivial_hyps.
apply eq_dec_implies_l4_17 with C D'; try assumption.
unfold Col; left.
apply between_exchange3 with A; try assumption.
apply eq_dec_implies_between_exchange4 with B; try assumption.
apply eq_dec_implies_between_exchange4 with D; assumption.
eapply eq_dec_implies_l4_17 with B B'; Cong.
unfold Col; right; left.
apply between_symmetry.
apply between_exchange3 with A; try assumption.
apply eq_dec_implies_between_exchange4 with D; assumption.
assert (Cong P P P Q).
apply eq_dec_implies_l4_17 with C C'; try assumption.
unfold Col; right; right.
apply between_symmetry; assumption.
(* Goal: or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
unfold IFSC,FSC, Cong_3 in *; spliter.
treat_equalities.
(* Goal: @Bet Tn A' B' C' *)
Between.
Qed.

Lemma eq_dec_implies_l5_2 :
  (forall A B:Tpoint, A=B \/ A<>B) ->
  forall A B C D,
  A<>B -> Bet A B C -> Bet A B D -> Bet B C D \/ Bet B D C.
Proof.
(* Goal: forall (x y : Prop) (_ : or (@eq Prop decidability_of_equality_of_points x) (or (@eq Prop decidability_of_congruence_of_points x) (or (@eq Prop decidability_of_betweenness_of_points x) False))) (_ : or (@eq Prop decidability_of_equality_of_points y) (or (@eq Prop decidability_of_congruence_of_points y) (or (@eq Prop decidability_of_betweenness_of_points y) False))), iff x y *)
intros.
(* Goal: or (@Bet Tn B C D) (@Bet Tn B D C) *)
assert (Bet A C D \/ Bet A D C) by (eapply eq_dec_implies_l5_1; eauto).
(* Goal: or (@Bet Tn B C D) (@Bet Tn B D C) *)
induction H3.
left; eBetween.
right; eBetween.
Qed.

Lemma eq_dec_implies_segment_construction_2 :
  (forall A B:Tpoint, A=B \/ A<>B) ->
  forall A Q B C, A<>Q -> exists X, (Bet Q A X \/ Bet Q X A) /\ Cong Q X B C.
Proof.
(* Goal: forall (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C : @Tpoint Tn), or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
intro eq_dec; intros.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (or (@Bet Tn Q A X) (@Bet Tn Q X A)) (@Cong Tn Q X B C)) *)
prolong A Q A' A Q.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (or (@Bet Tn Q A X) (@Bet Tn Q X A)) (@Cong Tn Q X B C)) *)
prolong A' Q X B C.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (or (@Bet Tn Q A X) (@Bet Tn Q X A)) (@Cong Tn Q X B C)) *)
exists X.
(* Goal: and (or (@Bet Tn Q A X) (@Bet Tn Q X A)) (@Cong Tn Q X B C) *)
show_distinct A' Q.
(* Goal: False *)
(* Goal: and (or (@Bet Tn Q A X) (@Bet Tn Q X A)) (@Cong Tn Q X B C) *)
solve [intuition].
(* Goal: and (or (@Bet Tn Q A X) (@Bet Tn Q X A)) (@Cong Tn Q X B C) *)
split; try assumption.
(* Goal: @Bet Tn A' B' C' *)
eapply (eq_dec_implies_l5_2 eq_dec A' Q); Between.
Qed.

Lemma eq_dec_implies_between_cong :
  (forall A B:Tpoint, A=B \/ A<>B) ->
  forall A B C, Bet A C B -> Cong A C A B -> C=B.
Proof.
(* Goal: forall (x y : Prop) (_ : or (@eq Prop decidability_of_equality_of_points x) (or (@eq Prop decidability_of_congruence_of_points x) (or (@eq Prop decidability_of_betweenness_of_points x) False))) (_ : or (@eq Prop decidability_of_equality_of_points y) (or (@eq Prop decidability_of_congruence_of_points y) (or (@eq Prop decidability_of_betweenness_of_points y) False))), iff x y *)
intros.
(* Goal: @eq (@Tpoint Tn) C B *)
assert (Bet A B C).
eapply eq_dec_implies_l4_6 with A C B; unfold Cong_3; repeat split; Cong.
eapply between_equality; eBetween.
Qed.

Lemma eq_dec_cong_dec :
  (forall A B:Tpoint, A=B \/ A<>B) ->
  (forall A B C D, Cong A B C D \/ ~ Cong A B C D).
Proof.
(* Goal: forall (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C : @Tpoint Tn), or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
intro eq_dec; intros.
(* Goal: or (@Cong Tn A B C D) (not (@Cong Tn A B C D)) *)
elim (eq_dec A B); intro; subst; elim (eq_dec C D); intro; subst.
left; Cong.
right; intro; apply H; apply cong_identity with B; Cong.
right; intro; apply H; apply cong_identity with D; Cong.
(* Goal: or (@Cong Tn A B C D) (not (@Cong Tn A B C D)) *)
elim (eq_dec_implies_segment_construction_2 eq_dec B A C D).
(* Goal: forall (x : @Tpoint Tn) (_ : and (or (@Bet Tn A B x) (@Bet Tn A x B)) (@Cong Tn A x C D)), or (@Cong Tn A B C D) (not (@Cong Tn A B C D)) *)
(* Goal: not (@eq (@Tpoint Tn) B A) *)
intros D' HD'.
(* Goal: or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
spliter.
(* Goal: or (@Cong Tn A B C D) (not (@Cong Tn A B C D)) *)
(* Goal: not (@eq (@Tpoint Tn) B A) *)
elim (eq_dec B D');intro.
(* Goal: or (@Cong Tn A B C D) (not (@Cong Tn A B C D)) *)
(* Goal: or (@Cong Tn A B C D) (not (@Cong Tn A B C D)) *)
(* Goal: not (@eq (@Tpoint Tn) B A) *)
subst; left; assumption.
(* Goal: or (@Cong Tn A B C D) (not (@Cong Tn A B C D)) *)
(* Goal: not (@eq (@Tpoint Tn) B A) *)
right; intro.
assert (Cong A D' A B) by eCong.
(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) B A) *)
elim H1; intro; clear H1.
(* Goal: False *)
(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) B A) *)
assert (B = D') by (apply (eq_dec_implies_between_cong eq_dec A D' B); Cong).
(* Goal: not (@eq (@Tpoint Tn) B A) *)
subst;intuition.
(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) B A) *)
assert (D'=B) by (apply (eq_dec_implies_between_cong eq_dec A B D');assumption).
(* Goal: not (@eq (@Tpoint Tn) B A) *)
subst;intuition.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
intuition.
Qed.

Lemma bet_dec_eq_dec :
  (forall A B C, Bet A B C \/ ~ Bet A B C) ->
  (forall A B:Tpoint, A=B \/ A<>B).
Proof.
(* Goal: forall (x y : Prop) (_ : or (@eq Prop decidability_of_equality_of_points x) (or (@eq Prop decidability_of_congruence_of_points x) (or (@eq Prop decidability_of_betweenness_of_points x) False))) (_ : or (@eq Prop decidability_of_equality_of_points y) (or (@eq Prop decidability_of_congruence_of_points y) (or (@eq Prop decidability_of_betweenness_of_points y) False))), iff x y *)
intros.
(* Goal: or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B)) *)
induction (H A B A).
(* Goal: or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B)) *)
(* Goal: or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B)) *)
left; apply between_identity; assumption.
right; intro; subst; apply H0;  apply between_trivial.
Qed.

Lemma eq_dec_implies_between_cong_3 :
  (forall A B:Tpoint, A=B \/ A<>B) ->
  forall A B D E, A <> B -> Bet A B D -> Bet A B E -> Cong B D B E -> D = E.
Proof.
(* Goal: forall (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C : @Tpoint Tn), or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
intro eq_dec; intros.
(* Goal: @eq (@Tpoint Tn) D E *)
assert (T:=eq_dec_implies_l5_2 eq_dec A B D E H H0 H1).
(* Goal: @eq (@Tpoint Tn) D E *)
elim T; intro; clear T.
apply eq_dec_implies_between_cong with B; Cong.
symmetry; apply eq_dec_implies_between_cong with B; Cong.
Qed.

Lemma eq_dec_bet_dec :
  (forall A B:Tpoint, A=B \/ A<>B) ->
  (forall A B C, Bet A B C \/ ~ Bet A B C).
Proof.
(* Goal: forall (_ : forall A B : @Tpoint Tn, or (@eq (@Tpoint Tn) A B) (not (@eq (@Tpoint Tn) A B))) (A B C : @Tpoint Tn), or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
intro eq_dec; intros.
(* Goal: or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
elim (segment_construction A B B C); intros C' HC'.
(* Goal: or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
spliter.
(* Goal: or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
elim (eq_dec C C'); intro.
(* Goal: not (@eq (@Tpoint Tn) E C) *)
subst; tauto.
(* Goal: or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
elim (eq_dec A B);intro.
(* Goal: @Bet Tn A' B' C' *)
left; subst; Between.
right; intro; apply H1; apply eq_dec_implies_between_cong_3 with A B; Cong.
Qed.

Definition decidability_of_equality_of_points := forall A B:Tpoint, A=B \/ A<>B.

Definition decidability_of_congruence_of_points := forall A B C D:Tpoint,
  Cong A B C D \/ ~ Cong A B C D.

Definition decidability_of_betweenness_of_points := forall A B C:Tpoint,
  Bet A B C \/ ~ Bet A B C.

Theorem equivalence_between_decidability_properties_of_basic_relations :
  all_equiv  (decidability_of_equality_of_points::
              decidability_of_congruence_of_points::
              decidability_of_betweenness_of_points::nil).
Proof.
(* Goal: all_equiv (@cons Prop decidability_of_equality_of_points (@cons Prop decidability_of_congruence_of_points (@cons Prop decidability_of_betweenness_of_points (@nil Prop)))) *)
unfold all_equiv.
(* Goal: forall (x y : Prop) (_ : @In Prop x (@cons Prop decidability_of_equality_of_points (@cons Prop decidability_of_congruence_of_points (@cons Prop decidability_of_betweenness_of_points (@nil Prop))))) (_ : @In Prop y (@cons Prop decidability_of_equality_of_points (@cons Prop decidability_of_congruence_of_points (@cons Prop decidability_of_betweenness_of_points (@nil Prop))))), iff x y *)
simpl.
(* Goal: forall (x y : Prop) (_ : or (@eq Prop decidability_of_equality_of_points x) (or (@eq Prop decidability_of_congruence_of_points x) (or (@eq Prop decidability_of_betweenness_of_points x) False))) (_ : or (@eq Prop decidability_of_equality_of_points y) (or (@eq Prop decidability_of_congruence_of_points y) (or (@eq Prop decidability_of_betweenness_of_points y) False))), iff x y *)
intros.
(* Goal: iff x y *)
assert (P:=cong_dec_eq_dec).
(* Goal: iff x y *)
assert (Q:=eq_dec_cong_dec).
(* Goal: iff x y *)
assert (R:=bet_dec_eq_dec).
(* Goal: iff x y *)
assert (S:=eq_dec_bet_dec).
(* Goal: not (@eq (@Tpoint Tn) E C) *)
decompose [or] H;clear H;decompose [or] H0;clear H0;subst; tauto.
Qed.

End Equivalence_between_decidability_properties_of_basic_relations.
