Require Export GeoCoq.Meta_theory.Decidability.equivalence_between_decidability_properties_of_basic_relations.

Section T5.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma l5_1 : 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 (A B C D : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : @Bet Tn A B C) (_ : @Bet Tn A B D), or (@Bet Tn A C D) (@Bet Tn A D C) *)
apply eq_dec_implies_l5_1; apply eq_dec_points.
Qed.

Lemma l5_2 : 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 (A B C D : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : @Bet Tn A B C) (_ : @Bet Tn A B D), or (@Bet Tn B C D) (@Bet Tn B D C) *)
apply eq_dec_implies_l5_2; apply eq_dec_points.
Qed.

Lemma segment_construction_2 :
  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 (A Q B C : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A Q)), @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)) *)
apply eq_dec_implies_segment_construction_2; apply eq_dec_points.
Qed.

Lemma l5_3 : forall A B C D,
 Bet A B D -> Bet A C D -> Bet A B C \/ Bet A C B.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
    assert (exists P, Bet D A P /\ A<>P) by  (apply point_construction_different).
(* Goal: or (@Bet Tn A B C) (@Bet Tn A C B) *)
    ex_and H1 P.
(* Goal: or (@Bet Tn A B C) (@Bet Tn A C B) *)
    assert (Bet P A B) by eBetween.
(* Goal: or (@Bet Tn A B C) (@Bet Tn A C B) *)
    assert (Bet P A C) by eBetween.
(* Goal: or (@Bet Tn A B C) (@Bet Tn A C B) *)
    apply (l5_2 P);auto.
Qed.

Lemma bet3__bet : forall A B C D E, Bet A B E -> Bet A D E -> Bet B C D -> Bet A C E.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: @Bet Tn A C E *)
    destruct (l5_3 A B D E H H0).
(* Goal: @Bet Tn A C E *)
(* Goal: @Bet Tn A C E *)
      apply between_exchange4 with D; trivial.
(* Goal: @Bet Tn A C D *)
(* Goal: @Bet Tn A C E *)
      apply between_exchange2 with B; assumption.
(* Goal: @Bet Tn A C E *)
    apply between_exchange4 with B; trivial.
(* Goal: @Bet Tn A C B *)
    apply between_exchange2 with D; Between.
Qed.

Lemma le_bet : forall A B C D, Le C D A B -> exists X, Bet A X B /\ Cong A X C D.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: @Cong Tn A B C D *)
    unfold Le in H.
(* Goal: @Cong Tn A B C D *)
    ex_and H Y.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A X B) (@Cong Tn A X C D)) *)
    exists Y;split;Cong.
Qed.

Lemma l5_5_1 : forall A B C D,
  Le A B C D -> exists x, Bet A B x /\ Cong A x C D.
Proof.
(* Goal: @Le Tn a' b' a' B *)
    unfold Le.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn C E D) (@Cong Tn B A C E)) *)
(* Goal: not (@Cong Tn B A C D) *)
    ex_and H P.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => and (@Bet Tn A B x) (@Cong Tn A x C D)) *)
    prolong A B x P D.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => and (@Bet Tn A B x) (@Cong Tn A x C D)) *)
    exists x.
(* Goal: @Lt Tn A A B C *)
    split.
(* Goal: @Le Tn A B C D *)
      assumption.
(* Goal: @Cong Tn A x C D *)
    eapply l2_11;eauto.
Qed.

Lemma l5_5_2 : forall A B C D,
 (exists x, Bet A B x /\ Cong A x C D) -> Le A B C D.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn C E D) (@Cong Tn B A C E)) *)
(* Goal: not (@Cong Tn B A C D) *)
    ex_and H P.
(* Goal: @Le Tn a' b' a' B *)
    unfold Le.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn C E D) (@Cong Tn A B C E)) *)
    assert (exists B' : Tpoint, Bet C B' D /\ Cong_3 A B P C B' D) by (eapply l4_5;auto).
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn C E D) (@Cong Tn A B C E)) *)
    ex_and H1 y.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn C E D) (@Cong Tn A B C E)) *)
    exists y.
(* Goal: and (@Bet Tn C y D) (@Cong Tn A B C y) *)
    unfold Cong_3 in *;intuition.
Qed.

Lemma l5_6 : forall A B C D A' B' C' D',
 Le A B C D -> Cong A B A' B' -> Cong C D C' D' -> Le A' B' C' D'.
Proof.
(* Goal: @Le Tn a' b' a' B *)
    unfold Le.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: and (@Le Tn B A C D) (not (@Cong Tn B A C D)) *)
    spliter.
(* Goal: @ex (@Tpoint Tn) (fun E0 : @Tpoint Tn => and (@Bet Tn E E0 F) (@Cong Tn A B E E0)) *)
    ex_and H y.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn C' E D') (@Cong Tn A' B' C' E)) *)
    assert (exists z : Tpoint, Bet C' z D' /\ Cong_3 C y D C' z D') by (eapply l4_5;auto).
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn C' E D') (@Cong Tn A' B' C' E)) *)
    ex_and H3 z.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn C' E D') (@Cong Tn A' B' C' E)) *)
    exists z.
(* Goal: @Lt Tn A A B C *)
    split.
(* Goal: @Le Tn A B C D *)
      assumption.
(* Goal: and (@Le Tn B A C D) (not (@Cong Tn B A C D)) *)
    unfold Cong_3 in *; spliter.
(* Goal: @Cong Tn A' B' C' z *)
    apply cong_transitivity with A B; try Cong.
(* Goal: @Le Tn A B C D *)
    apply cong_transitivity with C y; assumption.
Qed.

Lemma le_reflexivity : forall A B, Le A B A B.
Proof.
(* Goal: @Le Tn a' b' a' B *)
    unfold Le.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn C E A) (@Cong Tn C B C E)) *)
    exists B.
(* Goal: and (@Bet Tn C C D) (@Cong Tn A A C C) *)
    split; Between; Cong.
Qed.

Lemma le_transitivity : forall A B C D E F, Le A B C D -> Le C D E F -> Le A B E F.
Proof.
(* Goal: @Le Tn a' b' a' B *)
    unfold Le.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun E0 : @Tpoint Tn => and (@Bet Tn E E0 F) (@Cong Tn A B E E0)) *)
    ex_and H y.
(* Goal: @ex (@Tpoint Tn) (fun E0 : @Tpoint Tn => and (@Bet Tn E E0 F) (@Cong Tn A B E E0)) *)
    ex_and H0 z.
(* Goal: @ex (@Tpoint Tn) (fun E0 : @Tpoint Tn => and (@Bet Tn E E0 F) (@Cong Tn A B E E0)) *)
    assert (exists P : Tpoint, Bet E P z /\ Cong_3 C y D E P z) by (eapply l4_5;assumption).
(* Goal: @ex (@Tpoint Tn) (fun E0 : @Tpoint Tn => and (@Bet Tn E E0 F) (@Cong Tn A B E E0)) *)
    ex_and H3 P.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn C E D) (@Cong Tn B A C E)) *)
(* Goal: not (@Cong Tn B A C D) *)
    exists P.
(* Goal: @Lt Tn A A B C *)
    split.
(* Goal: @Bet Tn E P F *)
(* Goal: @Cong Tn A B E P *)
      eBetween.
(* Goal: @Cong Tn A B E P *)
    unfold Cong_3 in H4; spliter; apply cong_transitivity with C y; Cong.
Qed.

Lemma between_cong : forall A B C, Bet A C B -> Cong A C A B -> C=B.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Bet Tn A C B) (_ : @Cong Tn A C A B), @eq (@Tpoint Tn) C B *)
apply eq_dec_implies_between_cong; apply eq_dec_points.
Qed.

Lemma cong3_symmetry : forall A B C A' B' C' : Tpoint , Cong_3 A B C A' B' C' -> Cong_3 A' B' C' A B C.
Proof.
(* Goal: forall (A B C A' B' C' : @Tpoint Tn) (_ : @Cong_3 Tn A B C A' B' C'), @Cong_3 Tn A' B' C' A B C *)
    unfold Cong_3.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: False *)
    intuition.
Qed.

Lemma between_cong_2 : forall A B D E, Bet A D B -> Bet A E B -> Cong A D A E -> D = E.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: @eq (@Tpoint Tn) D E *)
    apply cong3_bet_eq with A B; unfold Cong_3; repeat split; Cong.
(* Goal: @Cong Tn E B D B *)
    eapply (l4_2 B E A B B D A B).
(* Goal: @IFSC Tn B E A B B D A B *)
    unfold IFSC; repeat split; Cong; Between.
Qed.

Lemma between_cong_3 :
  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 (A B D E : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : @Bet Tn A B D) (_ : @Bet Tn A B E) (_ : @Cong Tn B D B E), @eq (@Tpoint Tn) D E *)
apply eq_dec_implies_between_cong_3; apply eq_dec_points.
Qed.

Lemma le_anti_symmetry : forall A B C D, Le A B C D -> Le C D A B -> Cong A B C D.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: @Cong Tn A B C D *)
    assert (exists T, Bet C D T /\ Cong C T A B) by (apply l5_5_1;assumption).
(* Goal: @Cong Tn A B C D *)
    unfold Le in H.
(* Goal: @Cong Tn A B C D *)
    ex_and H Y.
(* Goal: @Cong Tn A B C D *)
    ex_and H1 T.
(* Goal: @Cong Tn A B C D *)
    assert (Cong C Y C T) by eCong.
(* Goal: @Bet Tn E P F *)
(* Goal: @Cong Tn A B E P *)
    assert (Bet C Y T) by eBetween.
(* Goal: @Cong Tn A B C D *)
    assert (Y=T) by (eapply between_cong;eauto).
(* Goal: @Cong Tn A B C D *)
    subst Y.
(* Goal: @Cong Tn A B C D *)
    assert (T=D) by (eapply between_equality;eBetween).
(* Goal: @Cong Tn A B C D *)
    subst T.
(* Goal: @Cong Tn O b'' b o *)
    Cong.
Qed.

Lemma cong_dec : forall A B C D,
  Cong A B C D \/ ~ Cong A B C D.
Proof.
(* Goal: forall A B C D : @Tpoint Tn, or (@Cong Tn A B C D) (not (@Cong Tn A B C D)) *)
apply eq_dec_cong_dec; apply eq_dec_points.
Qed.

Lemma bet_dec : forall A B C, Bet A B C  \/  ~ Bet A B C.
Proof.
(* Goal: forall A B C : @Tpoint Tn, or (@Bet Tn A B C) (not (@Bet Tn A B C)) *)
apply eq_dec_bet_dec; apply eq_dec_points.
Qed.

Lemma col_dec : forall A B C, Col A B C \/ ~ Col A B C.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: or (@Col Tn A B C) (not (@Col Tn A B C)) *)
    unfold Col.
(* Goal: or (or (@Bet Tn A B C) (or (@Bet Tn B C A) (@Bet Tn C A B))) (not (or (@Bet Tn A B C) (or (@Bet Tn B C A) (@Bet Tn C A B)))) *)
    elim (bet_dec A B C); intro; elim (bet_dec B C A); intro; elim (bet_dec C A B); intro; tauto.
Qed.


Lemma le_trivial : forall A C D, Le A A C D .
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: @Le Tn a' b' a' B *)
    unfold Le.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn C E D) (@Cong Tn A A C E)) *)
    exists C.
(* Goal: and (@Bet Tn C C D) (@Cong Tn A A C C) *)
    split; Between; Cong.
Qed.

Lemma le_cases : forall A B C D, Le A B C D \/ Le C D A B.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: or (@Le Tn A B C D) (@Le Tn C D A B) *)
    induction(eq_dec_points A B).
(* Goal: or (@Le Tn A B C D) (@Le Tn C D A B) *)
(* Goal: or (@Le Tn A B C D) (@Le Tn C D A B) *)
      subst B; left; apply le_trivial.
(* Goal: or (@Le Tn A B C D) (@Le Tn C D A B) *)
    assert (exists X : Tpoint, (Bet A B X \/ Bet A X B) /\ Cong A X C D) by (eapply (segment_construction_2 B A C D);auto).
(* Goal: or (@Le Tn A B C D) (@Le Tn C D A B) *)
    ex_and H0 X.
(* Goal: or (@Le Tn A B C D) (@Le Tn C D A B) *)
    induction H0.
(* Goal: @Le Tn A B C D *)
      left; apply l5_5_2; exists X; split; assumption.
(* Goal: @Cong Tn O b'' b o *)
    right; unfold Le; exists X; split; Cong.
Qed.

Lemma le_zero : forall A B C, Le A B C C -> A=B.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: @eq (@Tpoint Tn) A B *)
    assert (Le C C A B) by apply le_trivial.
(* Goal: @eq (@Tpoint Tn) A B *)
    assert (Cong A B C C) by (apply le_anti_symmetry;assumption).
(* Goal: @Le Tn a b A B *)
(* Goal: @Le Tn a b A B *)
    treat_equalities;auto.
Qed.

Lemma le_diff : forall A B C D, A <> B -> Le A B C D -> C <> D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : @Le Tn A B C D), not (@eq (@Tpoint Tn) C D) *)
  intros A B C D HAB HLe Heq.
(* Goal: @Le Tn A B C D *)
  subst D; apply HAB, le_zero with C; assumption.
Qed.

Lemma lt_diff : forall A B C D, Lt A B C D -> C <> D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Lt Tn A B C D), not (@eq (@Tpoint Tn) C D) *)
  intros A B C D HLt Heq.
(* Goal: False *)
  subst D.
(* Goal: False *)
  destruct HLt as [HLe HNCong].
(* Goal: False *)
  assert (A = B) by (apply le_zero with C; assumption).
(* Goal: @Cong Tn O b'' b o *)
  subst B; Cong.
Qed.

Lemma bet_cong_eq :
 forall A B C D,
  Bet A B C ->
  Bet A C D ->
  Cong B C A D ->
  C = D /\ A = B.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: and (@eq (@Tpoint Tn) C D) (@eq (@Tpoint Tn) A B) *)
    assert(C = D).
(* Goal: @eq (@Tpoint Tn) C D *)
(* Goal: and (@eq (@Tpoint Tn) C D) (@eq (@Tpoint Tn) A B) *)
      assert(Le A C A D) by (eapply l5_5_2; exists D; split; Cong).
(* Goal: @eq (@Tpoint Tn) C D *)
(* Goal: and (@eq (@Tpoint Tn) C D) (@eq (@Tpoint Tn) A B) *)
      assert(Le C B C A) by (eapply l5_5_2; exists A; split; Between; Cong).
(* Goal: @eq (@Tpoint Tn) C D *)
(* Goal: and (@eq (@Tpoint Tn) C D) (@eq (@Tpoint Tn) A B) *)
      assert(Cong A C A D) by (eapply le_anti_symmetry; try assumption; apply l5_6 with C B C A; Cong).
(* Goal: @Le Tn A B C D *)
      apply between_cong with A; assumption.
(* Goal: @Le Tn A B C D *)
    split; try assumption.
(* Goal: @eq (@Tpoint Tn) A B *)
    subst D; apply sym_equal.
(* Goal: @Cong Tn O b'' b o *)
    eapply (between_cong C); Between; Cong.
Qed.

Lemma cong__le : forall A B C D, Cong A B C D -> Le A B C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Cong Tn A B C D), @Le Tn A B C D *)
  intros A B C D H.
(* Goal: @Le Tn A B C D *)
  exists D.
(* Goal: @Lt Tn A A B C *)
  split.
(* Goal: @Bet Tn A P B *)
(* Goal: or (@Bet Tn P A B) (or (@Bet Tn A P B) (@Bet Tn A B P)) *)
  Between.
(* Goal: @Cong Tn O b'' b o *)
  Cong.
Qed.

Lemma cong__le3412 : forall A B C D, Cong A B C D -> Le C D A B.
Proof.
(* Goal: @Cong Tn O b'' b o *)
  intros A B C D HCong.
(* Goal: @Le Tn C D A B *)
  apply cong__le.
(* Goal: @Cong Tn O b'' b o *)
  Cong.
Qed.

Lemma le1221 : forall A B, Le A B B A.
Proof.
(* Goal: forall A B : @Tpoint Tn, @Le Tn A B B A *)
  intros A B.
(* Goal: @Cong Tn O b'' b o *)
  apply cong__le; Cong.
Qed.

Lemma le_left_comm : forall A B C D, Le A B C D -> Le B A C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Le Tn A B C D), @Le Tn A B D C *)
  intros A B C D Hle.
(* Goal: @Le Tn B A C D *)
  apply (le_transitivity _ _ A B); auto.
(* Goal: @Le Tn C D D C *)
  apply le1221; auto.
Qed.

Lemma le_right_comm : forall A B C D, Le A B C D -> Le A B D C.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Le Tn A B C D), @Le Tn A B D C *)
  intros A B C D Hle.
(* Goal: @Le Tn A B E F *)
(* Goal: not (@Cong Tn A B E F) *)
  apply (le_transitivity _ _ C D); auto.
(* Goal: @Le Tn C D D C *)
  apply le1221; auto.
Qed.

Lemma le_comm : forall A B C D, Le A B C D -> Le B A D C.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
  intros.
(* Goal: @Le Tn D C A B *)
  apply le_left_comm.
(* Goal: @Le Tn A B D C *)
(* Goal: not (@Cong Tn A B D C) *)
  apply le_right_comm.
(* Goal: @Le Tn A B C D *)
  assumption.
Qed.

Lemma ge_left_comm : forall A B C D, Ge A B C D -> Ge B A C D.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: @Ge Tn A B D C *)
    unfold Ge in *.
(* Goal: @Le Tn A B D C *)
(* Goal: not (@Cong Tn A B D C) *)
    apply le_right_comm.
(* Goal: @Le Tn A B C D *)
    assumption.
Qed.

Lemma ge_right_comm : forall A B C D, Ge A B C D -> Ge A B D C.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: @Ge Tn A B D C *)
    unfold Ge in *.
(* Goal: @Le Tn D C A B *)
    apply le_left_comm.
(* Goal: @Le Tn A B C D *)
    assumption.
Qed.

Lemma ge_comm :  forall A B C D, Ge A B C D -> Ge B A D C.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: @Ge Tn B A D C *)
    apply ge_left_comm.
(* Goal: @Ge Tn A B D C *)
    apply ge_right_comm.
(* Goal: @Le Tn A B C D *)
    assumption.
Qed.

Lemma lt_right_comm : forall A B C D, Lt A B C D -> Lt A B D C.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: @Lt Tn B A C D *)
    unfold Lt in *.
(* Goal: and (@Le Tn B A C D) (not (@Cong Tn B A C D)) *)
    spliter.
(* Goal: @Lt Tn A A B C *)
    split.
(* Goal: @Le Tn A B D C *)
(* Goal: not (@Cong Tn A B D C) *)
      apply le_right_comm.
(* Goal: @Le Tn A B C D *)
      assumption.
(* Goal: not (@Cong Tn A A B C) *)
    intro.
(* Goal: False *)
    apply H0.
(* Goal: @Cong Tn A B C D *)
    apply cong_right_commutativity.
(* Goal: @Le Tn A B C D *)
    assumption.
Qed.

Lemma lt_left_comm : forall A B  C D, Lt A B C D -> Lt B A C D.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: @Lt Tn B A C D *)
    unfold Lt in *.
(* Goal: and (@Le Tn B A C D) (not (@Cong Tn B A C D)) *)
    spliter.
(* Goal: @Lt Tn A A B C *)
    split.
(* Goal: @Le Tn B A C D *)
(* Goal: not (@Cong Tn B A C D) *)
      unfold Le in *.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn C E D) (@Cong Tn B A C E)) *)
(* Goal: not (@Cong Tn B A C D) *)
      ex_and H P.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn C E D) (@Cong Tn B A C E)) *)
(* Goal: not (@Cong Tn B A C D) *)
      exists P.
(* Goal: and (@Bet Tn C P D) (@Cong Tn B A C P) *)
(* Goal: not (@Cong Tn B A C D) *)
      apply cong_left_commutativity in H1.
(* Goal: @Le Tn A B C D *)
      split; assumption.
(* Goal: not (@Cong Tn A A B C) *)
    intro.
(* Goal: False *)
    apply H0.
(* Goal: @Cong Tn A B C D *)
    apply cong_left_commutativity.
(* Goal: @Le Tn A B C D *)
    assumption.
Qed.

Lemma lt_comm : forall A B  C D, Lt A B C D -> Lt B A D C.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: @Lt Tn D C A B *)
    apply lt_left_comm.
(* Goal: @Lt Tn C D B A *)
    apply lt_right_comm.
(* Goal: @Le Tn A B C D *)
    assumption.
Qed.

Lemma gt_left_comm : forall A B C D, Gt A B C D -> Gt B A C D.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: @Gt Tn A B D C *)
    unfold Gt in *.
(* Goal: @Lt Tn C D B A *)
    apply lt_right_comm.
(* Goal: @Le Tn A B C D *)
    assumption.
Qed.

Lemma gt_right_comm : forall A B C D, Gt A B C D -> Gt A B D C.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: @Gt Tn A B D C *)
    unfold Gt in *.
(* Goal: @Lt Tn D C A B *)
    apply lt_left_comm.
(* Goal: @Le Tn A B C D *)
    assumption.
Qed.

Lemma gt_comm : forall A B C D, Gt A B C D -> Gt B A D C.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: @Gt Tn B A D C *)
    apply gt_left_comm.
(* Goal: @Gt Tn A B D C *)
    apply gt_right_comm.
(* Goal: @Le Tn A B C D *)
    assumption.
Qed.

Lemma cong2_lt__lt : forall A B C D A' B' C' D',
 Lt A B C D -> Cong A B A' B' -> Cong C D C' D' -> Lt A' B' C' D'.
Proof.
(* Goal: forall (A B C D A' B' C' D' : @Tpoint Tn) (_ : @Lt Tn A B C D) (_ : @Cong Tn A B A' B') (_ : @Cong Tn C D C' D'), @Lt Tn A' B' C' D' *)
  intros A B C D A' B' C' D' Hlt HCong1 HCong2.
(* Goal: @Lt Tn A' B' C' D' *)
  destruct Hlt as [Hle HNCong].
(* Goal: @Lt Tn A A B C *)
  split.
(* Goal: @Le Tn A' B' C' D' *)
(* Goal: not (@Cong Tn A' B' C' D') *)
  apply (l5_6 A B C D); auto.
(* Goal: not (@Cong Tn A A B C) *)
  intro.
(* Goal: @Cong Tn O b'' b o *)
  apply HNCong.
(* Goal: @Cong Tn A B C D *)
  apply (cong_transitivity _ _ A' B'); auto.
(* Goal: @Cong Tn O b'' b o *)
  apply (cong_transitivity _ _ C' D'); Cong.
Qed.

Lemma fourth_point : forall A B C P, A <> B -> B <> C -> Col A B P -> Bet A B C ->
  Bet P A B \/ Bet A P B \/ Bet B P C \/ Bet B C P.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: or (@Bet Tn P A B) (or (@Bet Tn A P B) (or (@Bet Tn B P C) (@Bet Tn B C P))) *)
    induction H1.
(* Goal: or (@Bet Tn P A B) (or (@Bet Tn A P B) (or (@Bet Tn B P C) (@Bet Tn B C P))) *)
(* Goal: or (@Bet Tn P A B) (or (@Bet Tn A P B) (or (@Bet Tn B P C) (@Bet Tn B C P))) *)
      assert(HH:= l5_2 A B C P H H2 H1).
(* Goal: or (@Lt Tn A B C D) (or (@Gt Tn A B C D) (@Cong Tn A B C D)) *)
(* Goal: or (@Lt Tn A B C D) (or (@Gt Tn A B C D) (@Cong Tn A B C D)) *)
      right; right.
(* Goal: or (@Lt Tn A B C D) (or (@Gt Tn A B C D) (@Cong Tn A B C D)) *)
      induction HH.
(* Goal: or (@Bet Tn B P C) (@Bet Tn B C P) *)
(* Goal: or (@Bet Tn B P C) (@Bet Tn B C P) *)
(* Goal: or (@Bet Tn P A B) (or (@Bet Tn A P B) (or (@Bet Tn B P C) (@Bet Tn B C P))) *)
        right; auto.
(* Goal: or (@Bet Tn P A B) (or (@Bet Tn A P B) (or (@Bet Tn B P C) (@Bet Tn B C P))) *)
      left; auto.
(* Goal: or (@Bet Tn P A B) (or (@Bet Tn A P B) (or (@Bet Tn B P C) (@Bet Tn B C P))) *)
    induction H1.
(* Goal: or (@Lt Tn A B C D) (or (@Gt Tn A B C D) (@Cong Tn A B C D)) *)
      right; left.
(* Goal: @Bet Tn A P B *)
(* Goal: or (@Bet Tn P A B) (or (@Bet Tn A P B) (@Bet Tn A B P)) *)
      Between.
(* Goal: or (@Bet Tn P A B) (or (@Bet Tn A P B) (or (@Bet Tn B P C) (@Bet Tn B C P))) *)
    left; auto.
Qed.

Lemma third_point : forall A B P, Col A B P -> Bet P A B \/ Bet A P B \/ Bet A B P.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: or (@Bet Tn P A B) (or (@Bet Tn A P B) (@Bet Tn A B P)) *)
    induction H.
(* Goal: or (@Lt Tn A B C D) (or (@Gt Tn A B C D) (@Cong Tn A B C D)) *)
(* Goal: or (@Lt Tn A B C D) (or (@Gt Tn A B C D) (@Cong Tn A B C D)) *)
      right; right.
(* Goal: @Bet Tn P A B *)
      auto.
(* Goal: or (@Bet Tn P A B) (or (@Bet Tn A P B) (@Bet Tn A B P)) *)
    induction H.
(* Goal: or (@Lt Tn A B C D) (or (@Gt Tn A B C D) (@Cong Tn A B C D)) *)
      right; left.
(* Goal: @Bet Tn A P B *)
(* Goal: or (@Bet Tn P A B) (or (@Bet Tn A P B) (@Bet Tn A B P)) *)
      Between.
(* Goal: or (@Lt Tn A B C D) (or (@Gt Tn A B C D) (@Cong Tn A B C D)) *)
(* Goal: or (@Lt Tn A B C D) (or (@Gt Tn A B C D) (@Cong Tn A B C D)) *)
    left.
(* Goal: @Bet Tn P A B *)
    auto.
Qed.

Lemma l5_12_a : forall A B C, Bet A B C -> Le A B A C /\ Le B C A C.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: @Lt Tn A A B C *)
    split.
(* Goal: @Le Tn a' b' a' B *)
      unfold Le.
(* Goal: @Lt Tn A A B C *)
      exists B; split.
(* Goal: @Le Tn A B C D *)
        assumption.
(* Goal: @Cong Tn C B C B *)
      apply cong_reflexivity.
(* Goal: @Le Tn B C A C *)
    apply le_comm.
(* Goal: @Le Tn a' b' a' B *)
    unfold Le.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn C E A) (@Cong Tn C B C E)) *)
    exists B.
(* Goal: @Lt Tn A A B C *)
    split.
(* Goal: @Bet Tn C B A *)
(* Goal: @Cong Tn C B C B *)
      apply between_symmetry.
(* Goal: @Le Tn A B C D *)
      assumption.
(* Goal: @Cong Tn C B C B *)
    apply cong_reflexivity.
Qed.

Lemma bet__le1213 : forall A B C, Bet A B C -> Le A B A C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Bet Tn A B C), @Le Tn B C A C *)
    intros A B C HBet.
(* Goal: @Le Tn B C A C *)
    destruct (l5_12_a A B C HBet); trivial.
Qed.

Lemma bet__le2313 : forall A B C, Bet A B C -> Le B C A C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Bet Tn A B C), @Le Tn B C A C *)
    intros A B C HBet.
(* Goal: @Le Tn B C A C *)
    destruct (l5_12_a A B C HBet); trivial.
Qed.

Lemma bet__lt1213 : forall A B C, B <> C -> Bet A B C -> Lt A B A C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) B C)) (_ : @Bet Tn A B C), @Lt Tn A B A C *)
    intros A B C HBC HBet.
(* Goal: @Lt Tn A A B C *)
    split.
(* Goal: @Le Tn A B A C *)
(* Goal: not (@Cong Tn A B A C) *)
      apply bet__le1213; trivial.
(* Goal: not (@Cong Tn A A B C) *)
    intro.
(* Goal: False *)
    apply HBC, between_cong with A; trivial.
Qed.

Lemma bet__lt2313 : forall A B C, A <> B -> Bet A B C -> Lt B C A C.
Proof.
(* Goal: @Bet Tn A P B *)
(* Goal: or (@Bet Tn P A B) (or (@Bet Tn A P B) (@Bet Tn A B P)) *)
    intros; apply lt_comm, bet__lt1213; Between.
Qed.

Lemma l5_12_b : forall A B C, Col A B C -> Le A B A C -> Le B C A C -> Bet A B C.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
    unfold Col in H.
(* Goal: or (@Bet Tn P A B) (or (@Bet Tn A P B) (@Bet Tn A B P)) *)
    induction H.
(* Goal: @Le Tn A B C D *)
      assumption.
(* Goal: or (@Bet Tn P A B) (or (@Bet Tn A P B) (@Bet Tn A B P)) *)
    induction H.
      assert(Le B C B A /\ Le C A B A).
        apply l5_12_a.
(* Goal: @Le Tn A B C D *)
          assumption.
(* Goal: and (@Le Tn B A C D) (not (@Cong Tn B A C D)) *)
      spliter.
      assert(Cong A B A C).
        apply le_anti_symmetry.
(* Goal: @Le Tn A B C D *)
          assumption.
(* Goal: @Le Tn B C A C *)
        apply le_comm.
(* Goal: @Le Tn A B C D *)
        assumption.
      assert(C = B).
        eapply between_cong.
(* Goal: @Bet Tn C B A *)
(* Goal: @Cong Tn C B C B *)
          apply between_symmetry.
          apply H.
(* Goal: @Cong Tn A B C D *)
        apply cong_symmetry.
(* Goal: @Le Tn A B C D *)
        assumption.
      subst B.
      apply between_trivial.
    assert(Le B A B C /\ Le A C B C).
      apply l5_12_a.
(* Goal: @Bet Tn C B A *)
(* Goal: @Cong Tn C B C B *)
        apply between_symmetry.
(* Goal: @Le Tn A B C D *)
        assumption.
(* Goal: and (@Le Tn B A C D) (not (@Cong Tn B A C D)) *)
    spliter.
    assert(Cong B C A C).
      apply le_anti_symmetry.
(* Goal: @Le Tn A B C D *)
        assumption.
(* Goal: @Le Tn A B C D *)
      assumption.
    assert(A = B).
      eapply between_cong.
        apply H.
(* Goal: @Cong Tn A B C D *)
      apply cong_symmetry.
      apply cong_commutativity.
(* Goal: @Le Tn A B C D *)
      assumption.
    subst A.
(* Goal: @Bet Tn C B A *)
(* Goal: @Cong Tn C B C B *)
    apply between_symmetry.
    apply between_trivial.
Qed.

Lemma bet_le_eq : forall A B C, Bet A B C -> Le A C B C -> A = B.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
    assert(Le C B C A).
      eapply l5_5_2.
      exists A.
(* Goal: @Lt Tn A A B C *)
      split.
(* Goal: @Bet Tn C B A *)
(* Goal: @Cong Tn C B C B *)
        apply between_symmetry.
(* Goal: @Le Tn A B C D *)
        assumption.
(* Goal: @Cong Tn C B C B *)
      apply cong_reflexivity.
    assert(Cong A C B C).
      apply le_anti_symmetry.
(* Goal: @Le Tn A B C D *)
        assumption.
(* Goal: @Le Tn B C A C *)
      apply le_comm.
(* Goal: @Le Tn A B C D *)
      assumption.
    apply sym_equal.
    eapply between_cong.
(* Goal: @Bet Tn C B A *)
(* Goal: @Cong Tn C B C B *)
      apply between_symmetry.
      apply H.
    apply cong_commutativity.
(* Goal: @Cong Tn A B C D *)
    apply cong_symmetry.
(* Goal: @Le Tn A B C D *)
    assumption.
Qed.

Lemma or_lt_cong_gt : forall A B C D, Lt A B C D \/ Gt A B C D \/ Cong A B C D.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
    intros.
(* Goal: or (@Lt Tn A B C D) (or (@Gt Tn A B C D) (@Cong Tn A B C D)) *)
    assert(HH:= le_cases A B C D).
(* Goal: or (@Lt Tn A B C D) (or (@Gt Tn A B C D) (@Cong Tn A B C D)) *)
    induction HH.
(* Goal: or (@Lt Tn A B C D) (or (@Gt Tn A B C D) (@Cong Tn A B C D)) *)
      induction(cong_dec A B C D).
(* Goal: or (@Lt Tn A B C D) (or (@Gt Tn A B C D) (@Cong Tn A B C D)) *)
(* Goal: or (@Lt Tn A B C D) (or (@Gt Tn A B C D) (@Cong Tn A B C D)) *)
        right; right.
(* Goal: @Le Tn A B C D *)
        assumption.
(* Goal: or (@Lt Tn A B C D) (or (@Gt Tn A B C D) (@Cong Tn A B C D)) *)
(* Goal: or (@Lt Tn A B C D) (or (@Gt Tn A B C D) (@Cong Tn A B C D)) *)
      left.
(* Goal: @Lt Tn C D A B *)
      unfold Lt.
(* Goal: @Le Tn A B C D *)
      split; assumption.
(* Goal: or (@Lt Tn A B C D) (or (@Gt Tn A B C D) (@Cong Tn A B C D)) *)
    induction(cong_dec A B C D).
(* Goal: or (@Lt Tn A B C D) (or (@Gt Tn A B C D) (@Cong Tn A B C D)) *)
(* Goal: or (@Lt Tn A B C D) (or (@Gt Tn A B C D) (@Cong Tn A B C D)) *)
      right; right.
(* Goal: @Le Tn A B C D *)
      assumption.
(* Goal: or (@Lt Tn A B C D) (or (@Gt Tn A B C D) (@Cong Tn A B C D)) *)
    right; left.
(* Goal: @Gt Tn A B C D *)
    unfold Gt.
(* Goal: @Lt Tn C D A B *)
    unfold Lt.
(* Goal: @Lt Tn A A B C *)
    split.
(* Goal: @Le Tn A B C D *)
      assumption.
(* Goal: not (@Cong Tn A A B C) *)
    intro.
(* Goal: False *)
    apply H0.
(* Goal: @Cong Tn A B C D *)
    apply cong_symmetry.
(* Goal: @Le Tn A B C D *)
    assumption.
Qed.

Lemma lt__le : forall A B C D, Lt A B C D -> Le A B C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Lt Tn A B C D), @Le Tn A B C D *)
    intros A B C D Hlt.
(* Goal: @Le Tn A B C D *)
    destruct Hlt.
(* Goal: @Le Tn A B C D *)
    assumption.
Qed.

Lemma le1234_lt__lt : forall A B C D E F, Le A B C D -> Lt C D E F -> Lt A B E F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @Le Tn A B C D) (_ : @Lt Tn C D E F), @Lt Tn A B E F *)
    intros A B C D E F Hle Hlt.
(* Goal: @Lt Tn A B E F *)
    destruct Hlt as [Hle' HNCong].
(* Goal: @Lt Tn A A B C *)
    split.
(* Goal: @Le Tn A B E F *)
(* Goal: not (@Cong Tn A B E F) *)
      apply (le_transitivity _ _ C D); auto.
(* Goal: not (@Cong Tn A A B C) *)
    intro.
(* Goal: @Cong Tn O b'' b o *)
    apply HNCong.
(* Goal: @Bet Tn P A B *)
    apply le_anti_symmetry; auto.
(* Goal: @Cong Tn O b'' b o *)
    apply (l5_6 A B C D); Cong.
Qed.

Lemma le3456_lt__lt : forall A B C D E F, Lt A B C D -> Le C D E F -> Lt A B E F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @Lt Tn A B C D) (_ : @Le Tn C D E F), @Lt Tn A B E F *)
    intros A B C D E F Hlt Hle.
(* Goal: @Lt Tn A B E F *)
    destruct Hlt as [Hle' HNCong].
(* Goal: @Lt Tn A A B C *)
    split.
(* Goal: @Le Tn A B E F *)
(* Goal: not (@Cong Tn A B E F) *)
      apply (le_transitivity _ _ C D); auto.
(* Goal: not (@Cong Tn A A B C) *)
    intro.
(* Goal: @Cong Tn O b'' b o *)
    apply HNCong.
(* Goal: @Bet Tn P A B *)
    apply le_anti_symmetry; auto.
(* Goal: @Cong Tn O b'' b o *)
    apply (l5_6 C D E F); Cong.
Qed.

Lemma lt_transitivity : forall A B C D E F, Lt A B C D -> Lt C D E F -> Lt A B E F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @Lt Tn A B C D) (_ : @Lt Tn C D E F), @Lt Tn A B E F *)
    intros A B C D E F HLt1 HLt2.
(* Goal: @Le Tn A B C D *)
    apply le1234_lt__lt with C D; try (apply lt__le); assumption.
Qed.

Lemma not_and_lt : forall A B C D, ~ (Lt A B C D /\ Lt C D A B).
Proof.
(* Goal: forall A B C D : @Tpoint Tn, not (and (@Lt Tn A B C D) (@Lt Tn C D A B)) *)
    intros A B C D.
(* Goal: not (and (@Lt Tn A B C D) (@Lt Tn C D A B)) *)
    intro HInter.
(* Goal: False *)
    destruct HInter as [[Hle HNCong] []].
(* Goal: @Cong Tn O b'' b o *)
    apply HNCong.
(* Goal: @Le Tn A B C D *)
    apply le_anti_symmetry; assumption.
Qed.

Lemma nlt : forall A B, ~ Lt A B A B.
Proof.
(* Goal: forall A B : @Tpoint Tn, not (@Lt Tn A B A B) *)
    intros A B Hlt.
(* Goal: False *)
    apply (not_and_lt A B A B).
(* Goal: @Le Tn A B C D *)
    split; assumption.
Qed.

Lemma le__nlt : forall A B C D, Le A B C D -> ~ Lt C D A B.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Le Tn A B C D), not (@Lt Tn C D A B) *)
    intros A B C D HLe HLt.
(* Goal: @Bet Tn P A B *)
    apply (not_and_lt A B C D); split; auto.
(* Goal: @Bet Tn P A B *)
    split; auto.
(* Goal: not (@Cong Tn A B C D) *)
    unfold Lt in *; spliter; auto with cong.
Qed.

Lemma cong__nlt : forall A B C D,
 Cong A B C D -> ~ Lt A B C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Cong Tn A B C D), not (@Lt Tn A B C D) *)
    intros P Q R S H.
(* Goal: not (@Lt Tn P Q R S) *)
    apply le__nlt.
(* Goal: @Le Tn a' b' a' B *)
    unfold Le.
(* Goal: @Bet Tn A P B *)
(* Goal: or (@Bet Tn P A B) (or (@Bet Tn A P B) (@Bet Tn A B P)) *)
    exists Q; split; Cong; Between.
Qed.

Lemma nlt__le : forall A B C D, ~ Lt A B C D -> Le C D A B.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : not (@Lt Tn A B C D)), @Le Tn C D A B *)
    intros A B C D HNLt.
(* Goal: @Le Tn C D A B *)
    destruct (le_cases A B C D); trivial.
(* Goal: @Le Tn C D A B *)
    destruct (cong_dec C D A B).
(* Goal: @Le Tn A B C D *)
      apply cong__le; assumption.
(* Goal: @Le Tn C D A B *)
    exfalso.
(* Goal: False *)
    apply HNLt.
(* Goal: @Cong Tn O b'' b o *)
    split; Cong.
Qed.

Lemma lt__nle : forall A B C D, Lt A B C D -> ~ Le C D A B.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Lt Tn A B C D), not (@Le Tn C D A B) *)
  intros A B C D HLt HLe.
(* Goal: False *)
  generalize HLt.
(* Goal: @Le Tn A B C D *)
  apply le__nlt; assumption.
Qed.

Lemma nle__lt : forall A B C D, ~ Le A B C D -> Lt C D A B.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : not (@Le Tn A B C D)), @Lt Tn C D A B *)
    intros A B C D HNLe.
(* Goal: @Lt Tn C D A B *)
    destruct (le_cases A B C D).
(* Goal: @Lt Tn C D A B *)
(* Goal: @Lt Tn C D A B *)
      contradiction.
(* Goal: @Lt Tn C D A B *)
    split; trivial.
(* Goal: not (@Cong Tn A A B C) *)
    intro.
(* Goal: False *)
    apply HNLe.
(* Goal: @Cong Tn O b'' b o *)
    apply cong__le; Cong.
Qed.

Lemma lt1123 : forall A B C, B<>C -> Lt A A B C.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
intros.
(* Goal: @Lt Tn A A B C *)
split.
(* Goal: @Le Tn A A B C *)
(* Goal: not (@Cong Tn A A B C) *)
apply le_trivial.
(* Goal: not (@Cong Tn A A B C) *)
intro.
(* Goal: @Le Tn a b A B *)
treat_equalities.
(* Goal: False *)
intuition.
Qed.

Lemma bet2_le2__le : forall O o A B a b, Bet a o b -> Bet A O B -> Le o a O A -> Le o b O B -> Le a b A B.
Proof.
(* Goal: forall (O o A B a b : @Tpoint Tn) (_ : @Bet Tn a o b) (_ : @Bet Tn A O B) (_ : @Le Tn o a O A) (_ : @Le Tn o b O B), @Le Tn a b A B *)
intros.
(* Goal: @Le Tn a b A B *)
induction(eq_dec_points A O).
(* Goal: @Bet Tn P A B *)
treat_equalities; auto.
(* Goal: @Le Tn a b A B *)
(* Goal: @Le Tn a b A B *)
assert (o=a). 
(* Goal: @Bet Tn P A B *)
apply le_zero with A;auto.
(* Goal: @Bet Tn P A B *)
subst;auto.
(* Goal: @Le Tn a b A B *)
induction(eq_dec_points B O).
(* Goal: @Le Tn a b A B *)
(* Goal: @Le Tn a b A B *)
treat_equalities;auto.
(* Goal: @Le Tn a b A B *)
(* Goal: @Le Tn a b A B *)
assert (o=b). 
(* Goal: @Bet Tn P A B *)
apply le_zero with B;auto.
(* Goal: @Le Tn a b A B *)
(* Goal: @Le Tn a b A B *)
subst;auto using le_left_comm, le_right_comm.


(* Goal: @Le Tn a b A B *)
assert(HH:= segment_construction A O b o).
(* Goal: @Le Tn a b A B *)
ex_and HH b'.
(* Goal: @Le Tn a b A B *)
assert(HH:= segment_construction B O a o).
(* Goal: @Le Tn a b A B *)
ex_and HH a'.

(* Goal: @Le Tn a b A B *)
unfold Le in H1.
(* Goal: @Le Tn a b A B *)
ex_and H1 a''.

(* Goal: @Le Tn a b A B *)
assert(a' = a'').
(* Goal: @Le Tn a' b' A B *)
(* Goal: @Le Tn a b A B *)
{
  apply(construction_uniqueness B O a o a' a'' H4);
(* Goal: @Bet Tn E P F *)
(* Goal: @Cong Tn A B E P *)
  eBetween.
(* Goal: @Cong Tn O b'' b o *)
  Cong.
}
(* Goal: @Le Tn a b A B *)
treat_equalities.

(* Goal: @Le Tn a b A B *)
assert(Le B a' B A).
(* Goal: @Le Tn a' b' A B *)
(* Goal: @Le Tn a b A B *)
{
(* Goal: @Le Tn a' b' a' B *)
  unfold Le.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn B E A) (@Cong Tn B a' B E)) *)
  exists a'.
(* Goal: @Cong Tn O b'' b o *)
  split; eBetween; Cong.
}

(* Goal: @Le Tn a b A B *)
unfold Le in H2.
(* Goal: @Le Tn a b A B *)
ex_and H2 b''.

(* Goal: @Le Tn a b A B *)
assert(b' = b'').
(* Goal: @Le Tn a' b' A B *)
(* Goal: @Le Tn a b A B *)
{
  apply(construction_uniqueness A O b o b' b'' H3);
(* Goal: @Bet Tn E P F *)
(* Goal: @Cong Tn A B E P *)
  eBetween.
(* Goal: @Cong Tn O b'' b o *)
  Cong.
}

(* Goal: @Le Tn a b A B *)
treat_equalities.

(* Goal: @Le Tn a b A B *)
assert(Le a' b' a' B).
(* Goal: @Le Tn a' b' A B *)
(* Goal: @Le Tn a b A B *)
{
(* Goal: @Le Tn a' b' a' B *)
  unfold Le.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn a' E B) (@Cong Tn a' b' a' E)) *)
  exists b'.
(* Goal: @Cong Tn O b'' b o *)
  split; eBetween; Cong.
}

(* Goal: @Le Tn a b A B *)
assert(Le a' b' A B).
(* Goal: @Le Tn a' b' A B *)
(* Goal: @Le Tn a b A B *)
{
(* Goal: @Le Tn a' b' A B *)
  apply(le_transitivity a' b' a' B A B); auto using le_left_comm, le_right_comm.
}

(* Goal: @Cong Tn O b'' b o *)
apply(l5_6 a' b' A B a b A B); Cong.
apply (l2_11 a' O b' a o b);
(* Goal: @Cong Tn O b'' b o *)
eBetween; Cong.
Qed.

End T5.

Hint Resolve le_reflexivity le_anti_symmetry le_trivial le_zero cong__le cong__le3412
             le1221 le_left_comm le_right_comm le_comm lt__le bet__le1213 bet__le2313
             lt_left_comm lt_right_comm lt_comm bet__lt1213 bet__lt2313 lt1123 : le.

Ltac Le := auto with le.
