Require Export GeoCoq.Tarski_dev.Ch05_bet_le.

Ltac eCol := eauto with col.

Section T6_1.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma bet_out : forall A B C, B <> A -> Bet A B C -> Out A B C.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: forall (P A B : @Tpoint Tn) (_ : @Out Tn P A B) (_ : @Le Tn P A P B), @Bet Tn P A B *)
    unfold Out.
(* Goal: and (not (@eq (@Tpoint Tn) B A)) (and (not (@eq (@Tpoint Tn) C A)) (or (@Bet Tn A B C) (@Bet Tn A C B))) *)
    repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) C A) *)
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@Bet Tn A B' C) (@Cong Tn C B' A B)) *)
    intro; treat_equalities; auto.
Qed.

Lemma out_dec : forall P A B, Out P A B \/ ~ Out P A B.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: forall (P A B : @Tpoint Tn) (_ : @Out Tn P A B) (_ : @Le Tn P A P B), @Bet Tn P A B *)
    unfold Out.
(* Goal: or (and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A)))) (not (and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))))) *)
    elim (bet_dec P A B);intro; elim (bet_dec P B A);intro; elim (eq_dec_points A P);intro; elim (eq_dec_points B P);intro; tauto.
Qed.

Lemma out_diff1 : forall A B C, Out A B C -> B <> A.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: or (@Bet Tn A B C) (or (@Bet Tn B C A) (@Bet Tn C A B)) *)
    unfold Out in H.
(* Goal: False *)
    spliter.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    assumption.
Qed.

Lemma out_diff2 : forall A B C, Out A B C -> C <> A.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: or (@Bet Tn A B C) (or (@Bet Tn B C A) (@Bet Tn C A B)) *)
    unfold Out in H.
(* Goal: False *)
    spliter.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    assumption.
Qed.

Lemma out_distinct : forall A B C, Out A B C -> B <> A /\ C <> A.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C)) *)
    split.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) C A) *)
      eapply out_diff1;eauto.
(* Goal: not (@eq (@Tpoint Tn) C A) *)
    eapply out_diff2;eauto.
Qed.

Lemma out_col : forall A B C, Out A B C -> Col A B C.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: @Col Tn X P S *)
    unfold Col.
(* Goal: or (@Bet Tn A B C) (or (@Bet Tn B C A) (@Bet Tn C A B)) *)
    unfold Out in H.
(* Goal: False *)
    spliter.
(* Goal: or (@Bet Tn A B C) (or (@Bet Tn B C A) (@Bet Tn C A B)) *)
    induction H1;Between.
Qed.

Lemma l6_2 : forall A B C P,  A<>P -> B<>P -> C<>P -> Bet A P C -> (Bet B P C <-> Out P A B).
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: forall (P A B : @Tpoint Tn) (_ : @Out Tn P A B) (_ : @Le Tn P A P B), @Bet Tn P A B *)
    unfold Out.
(* Goal: and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C)) *)
    split.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
      intros.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
      repeat split; try assumption; eapply l5_2;eBetween.
(* Goal: forall _ : and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))), @Bet Tn B P C *)
    intro; spliter; induction H5; eBetween.
Qed.

Lemma bet_out__bet : forall A B C P, Bet A P C -> Out P A B -> Bet B P C.
Proof.
(* Goal: forall (A B C P : @Tpoint Tn) (_ : @Bet Tn A P C) (_ : @Out Tn P A B), @Bet Tn B P C *)
    intros A B C P HBet HOut.
(* Goal: @Bet Tn B P C *)
    destruct (eq_dec_points C P).
(* Goal: @Bet Tn B P C *)
(* Goal: @Bet Tn B P C *)
      subst; Between.
(* Goal: @Bet Tn B P C *)
    apply (l6_2 A); trivial; destruct HOut as [HPA [HPB]]; auto.
Qed.

Lemma l6_3_1 : forall A B P, Out P A B -> (A<>P /\ B<>P /\ exists C, C<>P /\ Bet A P C /\ Bet B P C).
Proof.
(* Goal: forall (P A B : @Tpoint Tn) (_ : @Out Tn P A B) (_ : @Le Tn P A P B), @Bet Tn P A B *)
    unfold Out.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: False *)
    spliter.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    repeat split; try assumption.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C P)) (and (@Bet Tn A P C) (@Bet Tn B P C))) *)
    induction H1.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C P)) (and (@Bet Tn A P C) (@Bet Tn B P C))) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C P)) (and (@Bet Tn A P C) (@Bet Tn B P C))) *)
      assert(exists C, Bet A P C /\ P <> C) by (apply point_construction_different).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C P)) (and (@Bet Tn A P C) (@Bet Tn B P C))) *)
      ex_and H2 C.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
      exists C.
(* Goal: and (not (@eq (@Tpoint Tn) C P)) (and (@Bet Tn A P C) (@Bet Tn B P C)) *)
      repeat split; eBetween.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C P)) (and (@Bet Tn A P C) (@Bet Tn B P C))) *)
    assert(exists C, Bet B P C /\ P <> C) by (apply point_construction_different).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C P)) (and (@Bet Tn A P C) (@Bet Tn B P C))) *)
    ex_and H2 C.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    exists C.
(* Goal: and (not (@eq (@Tpoint Tn) C P)) (and (@Bet Tn A P C) (@Bet Tn B P C)) *)
    repeat split;eBetween.
Qed.

Lemma l6_3_2 : forall A B P,
  (A<>P /\ B<>P /\ exists C, C<>P /\ Bet A P C /\ Bet B P C) -> Out P A B.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: False *)
    spliter.
(* Goal: @Out Tn P A B *)
    ex_and H1 C.
(* Goal: forall (P A B : @Tpoint Tn) (_ : @Out Tn P A B) (_ : @Le Tn P A P B), @Bet Tn P A B *)
    unfold Out.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
    repeat split; try assumption; eapply l5_2; eBetween.
Qed.

Lemma l6_4_1 : forall A B P, Out P A B -> Col A P B /\ ~ Bet A P B.
Proof.
(* Goal: forall (P A B : @Tpoint Tn) (_ : @Out Tn P A B) (_ : @Le Tn P A P B), @Bet Tn P A B *)
    unfold Out.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: False *)
    spliter.
(* Goal: @Col Tn X P S *)
    unfold Col.
(* Goal: and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C)) *)
    induction H1; split.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      Between.
(* Goal: not (@Bet Tn A P B) *)
(* Goal: or (@Bet Tn A P B) (or (@Bet Tn P B A) (@Bet Tn B A P)) *)
(* Goal: not (@Bet Tn A P B) *)
      intro; apply H; eapply between_equality;eauto.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      right; left; assumption.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    intro; apply H0; eapply between_equality; eBetween.
Qed.

Lemma l6_4_2 : forall A B P, Col A P B /\ ~ Bet A P B -> Out P A B.
Proof.
(* Goal: @Col Tn X P S *)
    unfold Col.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: False *)
    spliter.
(* Goal: forall (P A B : @Tpoint Tn) (_ : @Out Tn P A B) (_ : @Le Tn P A P B), @Bet Tn P A B *)
    unfold Out.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
    induction H.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
      contradiction.
(* Goal: @Col Tn P A B *)
    induction (eq_dec_points A P).
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
      subst P; intuition.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
    induction (eq_dec_points B P).
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
      subst P; intuition.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    induction H; repeat split; Between.
Qed.

(** out reflexivity. l6_5 *)

Lemma out_trivial : forall P A, A<>P -> Out P A A.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: forall (P A B : @Tpoint Tn) (_ : @Out Tn P A B) (_ : @Le Tn P A P B), @Bet Tn P A B *)
    unfold Out.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    repeat split; Between.
Qed.

(** out symmetry. *)

Lemma l6_6 : forall P A B, Out P A B -> Out P B A.
Proof.
(* Goal: forall (P A B : @Tpoint Tn) (_ : @Out Tn P A B) (_ : @Le Tn P A P B), @Bet Tn P A B *)
    unfold Out.
(* Goal: False *)
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    intuition.
Qed.

(** out transitivity. *)

Lemma l6_7 : forall P A B C, Out P A B -> Out P B C -> Out P A C.
Proof.
(* Goal: forall (P A B : @Tpoint Tn) (_ : @Out Tn P A B) (_ : @Le Tn P A P B), @Bet Tn P A B *)
    unfold Out.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: False *)
    spliter.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    repeat split; try assumption.
(* Goal: or (@Bet Tn P A C) (@Bet Tn P C A) *)
    induction H4; induction H2.
(* Goal: or (@Bet Tn P A C) (@Bet Tn P C A) *)
(* Goal: or (@Bet Tn P A C) (@Bet Tn P C A) *)
(* Goal: or (@Bet Tn P A C) (@Bet Tn P C A) *)
(* Goal: or (@Bet Tn P A C) (@Bet Tn P C A) *)
      left; eapply between_exchange4; eauto.
(* Goal: or (@Bet Tn P A C) (@Bet Tn P C A) *)
(* Goal: or (@Bet Tn P A C) (@Bet Tn P C A) *)
(* Goal: or (@Bet Tn P A C) (@Bet Tn P C A) *)
      eapply l5_3; eauto.
(* Goal: or (@Bet Tn P A C) (@Bet Tn P C A) *)
(* Goal: or (@Bet Tn P A C) (@Bet Tn P C A) *)
      eapply (l5_1 P B); auto.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    right; eBetween.
Qed.

Lemma bet_out_out_bet : forall A B C A' C',
 Bet A B C -> Out B A A' -> Out B C C' -> Bet A' B C'.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: and (@Out Tn B A P) (@Out Tn B C P) *)
    unfold Out in *.
(* Goal: False *)
    spliter.
(* Goal: and (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) P B)) (or (@Bet Tn B A P) (@Bet Tn B P A)))) (and (not (@eq (@Tpoint Tn) C B)) (and (not (@eq (@Tpoint Tn) P B)) (or (@Bet Tn B C P) (@Bet Tn B P C)))) *)
    induction H5; induction H3.
(* Goal: @Bet Tn A' B C' *)
(* Goal: @Bet Tn A' B C' *)
(* Goal: @Bet Tn A' B C' *)
      assert(Bet A' B C) by (apply outer_transitivity_between2 with A; Between).
(* Goal: @Bet Tn A' B C' *)
(* Goal: @Bet Tn A' B C' *)
      apply outer_transitivity_between with C; auto.
(* Goal: @Bet Tn A' B C' *)
(* Goal: @Bet Tn A' B C' *)
(* Goal: @Bet Tn A' B C' *)
      assert(Bet A' B C) by (apply outer_transitivity_between2 with A; Between).
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      apply between_inner_transitivity with C; assumption.
(* Goal: @Bet Tn A' B C' *)
      assert(Bet A' B C) by (apply between_exchange3 with A; Between).
(* Goal: @Bet Tn A' B C' *)
(* Goal: @Bet Tn A' B C' *)
      apply outer_transitivity_between with C; auto.
(* Goal: @Bet Tn A' B C' *)
    assert(Bet A' B C) by (apply between_exchange3 with A; Between).
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    eapply between_inner_transitivity with C; assumption.
Qed.

Lemma out2_bet_out : forall A B C X P,
 Out B A C -> Out B X P -> Bet A X C -> Out B A P /\ Out B C P.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: and (@Out Tn B A P) (@Out Tn B C P) *)
    unfold Out in *.
(* Goal: False *)
    spliter.
(* Goal: and (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) P B)) (or (@Bet Tn B A P) (@Bet Tn B P A)))) (and (not (@eq (@Tpoint Tn) C B)) (and (not (@eq (@Tpoint Tn) P B)) (or (@Bet Tn B C P) (@Bet Tn B P C)))) *)
    induction H5; induction H3.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      repeat split; try assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        left; eapply between_exchange4 with X; try assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        apply between_inner_transitivity with C; assumption.
(* Goal: or (@Bet Tn B A P) (@Bet Tn B P A) *)
(* Goal: or (@Bet Tn B C P) (@Bet Tn B P C) *)
(* Goal: and (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) P B)) (or (@Bet Tn B A P) (@Bet Tn B P A)))) (and (not (@eq (@Tpoint Tn) C B)) (and (not (@eq (@Tpoint Tn) P B)) (or (@Bet Tn B C P) (@Bet Tn B P C)))) *)
      apply l5_1 with X; try auto.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      apply between_exchange2 with A; assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      repeat split; try assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        apply l5_3 with X; try assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        apply between_inner_transitivity with C; assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      right; apply between_exchange4 with X; try assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      apply between_exchange2 with A; assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      repeat split; try assumption.
(* Goal: or (@Bet Tn B A P) (@Bet Tn B P A) *)
(* Goal: or (@Bet Tn B C P) (@Bet Tn B P C) *)
(* Goal: and (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) P B)) (or (@Bet Tn B A P) (@Bet Tn B P A)))) (and (not (@eq (@Tpoint Tn) C B)) (and (not (@eq (@Tpoint Tn) P B)) (or (@Bet Tn B C P) (@Bet Tn B P C)))) *)
        apply l5_1 with X; try auto.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
        apply between_exchange2 with C; Between.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      left; apply between_exchange4 with X; try assumption.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      apply between_inner_transitivity with A; Between.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    repeat split; try assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      right; apply between_exchange4 with X; try assumption.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      apply between_exchange2 with C; Between.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    apply l5_3 with X; try assumption.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    apply between_inner_transitivity with A; Between.
Qed.

Lemma l6_11_uniqueness : forall A B C R X Y,
  R<>A -> B<>C ->
  Out A X R -> Cong A X B C ->
  Out A Y R -> Cong A Y B C ->
  X=Y.
Proof.
(* Goal: forall (P A B : @Tpoint Tn) (_ : @Out Tn P A B) (_ : @Le Tn P A P B), @Bet Tn P A B *)
    unfold Out.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: False *)
    spliter.
(* Goal: @eq (@Tpoint Tn) X Y *)
    assert (Cong A X A Y) by eCong.
(* Goal: @eq (@Tpoint Tn) X Y *)
    induction H8; induction H6.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      apply l4_19 with A R; try assumption.
(* Goal: @Cong Tn R X R Y *)
(* Goal: @eq (@Tpoint Tn) X Y *)
(* Goal: @eq (@Tpoint Tn) X Y *)
(* Goal: @eq (@Tpoint Tn) X Y *)
      apply l4_3 with A A; Between; Cong.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      assert (Bet A X Y) by eBetween.
(* Goal: @eq (@Tpoint Tn) X Y *)
(* Goal: @eq (@Tpoint Tn) X Y *)
(* Goal: @eq (@Tpoint Tn) X Y *)
      eapply between_cong; eauto.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      assert (Bet A Y X) by eBetween.
(* Goal: @eq (@Tpoint Tn) X Y *)
      apply sym_equal; apply between_cong with A; Cong.
(* Goal: @eq (@Tpoint Tn) X Y *)
    assert (Bet A X Y \/ Bet A Y X) by (eapply l5_1; eauto).
(* Goal: @eq (@Tpoint Tn) X Y *)
    induction H10.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      apply between_cong with A; assumption.
(* Goal: @eq (@Tpoint Tn) X Y *)
    apply sym_equal; apply between_cong with A; Cong.
Qed.

Lemma l6_11_existence : forall A B C R,
  R<>A -> B<>C -> exists X, Out A X R /\ Cong A X B C.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Out Tn A X R) (@Cong Tn A X B C)) *)
    assert (exists X : Tpoint, (Bet A R X \/ Bet A X R) /\ Cong A X B C) by (apply (segment_construction_2);assumption).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Out Tn A X R) (@Cong Tn A X B C)) *)
    ex_and H1 X.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Out Tn A X R) (@Cong Tn A X B C)) *)
    exists X.
(* Goal: False *)
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    unfold Out;repeat split; try intro;treat_equalities;intuition.
Qed.

Lemma segment_construction_3 : forall A B X Y, A <> B -> X <> Y -> exists C, Out A B C /\ Cong A C X Y.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Out Tn A B C) (@Cong Tn A C X Y)) *)
    destruct (l6_11_existence A X Y B) as [C [HC1 HC2]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Out Tn A B C) (@Cong Tn A C X Y)) *)
    apply l6_6 in HC1.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Out Tn A B C) (@Cong Tn A C X Y)) *)
    exists C; auto.
Qed.

Lemma l6_13_1 : forall P A B, Out P A B -> Le
 P A P B -> Bet P A B.
Proof.
(* Goal: forall (P A B : @Tpoint Tn) (_ : @Out Tn P A B) (_ : @Le Tn P A P B), @Bet Tn P A B *)
    unfold Out.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: False *)
    spliter.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    induction H2; try assumption.
    unfold Le
 in H0.
(* Goal: @Bet Tn P A B *)
    ex_and H0 Y.
(* Goal: @Bet Tn P A B *)
    assert(Y = A).
(* Goal: @eq (@Tpoint Tn) Y A *)
(* Goal: @Bet Tn P A B *)
      apply (l6_11_uniqueness P P A B); Between; Cong.
(* Goal: and (not (@eq (@Tpoint Tn) B A)) (and (not (@eq (@Tpoint Tn) C A)) (or (@Bet Tn A B C) (@Bet Tn A C B))) *)
        unfold Out; repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) C A) *)
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@Bet Tn A B' C) (@Cong Tn C B' A B)) *)
        intro; treat_equalities; auto.
(* Goal: and (not (@eq (@Tpoint Tn) B A)) (and (not (@eq (@Tpoint Tn) C A)) (or (@Bet Tn A B C) (@Bet Tn A C B))) *)
      unfold Out; repeat split; auto.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    subst Y; assumption.
Qed.

Lemma l6_13_2 : forall P A B, Out P A B -> Bet P A B -> Le
 P A P B.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: @Le Tn P A P B *)
    unfold Le.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn P E B) (@Cong Tn P A P E)) *)
    exists A.
(* Goal: and (@Bet Tn P A B) (@Cong Tn P A P A) *)
    split; Cong.
Qed.

Lemma l6_16_1 : forall P Q S X, P<>Q -> Col S P Q -> Col X P Q -> Col X P S.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: @Col Tn X P S *)
    destruct (eq_dec_points S P).
(* Goal: @Col Tn X Y C *)
(* Goal: @Col Tn X Y C *)
      subst; Col.
(* Goal: @Col Tn X P S *)
    assert((Bet P S X \/ Bet P X S) -> (Bet P S X \/ Bet S X P)) by (intro; induction H3; Between).
(* Goal: @Col Tn X P S *)
    unfold Col.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C P)) (and (@Bet Tn A P C) (@Bet Tn B P C))) *)
    induction H0;induction H1.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      right; apply H3; eapply (l5_2 Q P); Between.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      induction H1; left; eBetween.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      induction H0; left; eBetween.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C P)) (and (@Bet Tn A P C) (@Bet Tn B P C))) *)
    induction H0; induction H1.
(* Goal: or (@Bet Tn X P S) (or (@Bet Tn P S X) (@Bet Tn S X P)) *)
(* Goal: or (@Bet Tn X P S) (or (@Bet Tn P S X) (@Bet Tn S X P)) *)
(* Goal: or (@Bet Tn X P S) (or (@Bet Tn P S X) (@Bet Tn S X P)) *)
(* Goal: or (@Bet Tn X P S) (or (@Bet Tn P S X) (@Bet Tn S X P)) *)
      right; apply H3; eapply l5_1; eauto.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      right; right; eBetween.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      right; left; eBetween.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    right; apply H3; eapply l5_3; eBetween.
Qed.

Lemma col_transitivity_1 : forall P Q A B,
  P<>Q -> Col P Q A -> Col P Q B -> Col P A B.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: @Col Tn P A B *)
    induction (eq_dec_points A P).
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      subst; unfold Col; Between.
(* Goal: @Col Tn P A B *)
    assert (T:=l6_16_1 P Q A B).
(* Goal: @Col Tn P A B *)
    apply col_permutation_1; apply T; Col.
Qed.

Lemma col_transitivity_2 : forall P Q A B,
 P<>Q -> Col P Q A -> Col P Q B -> Col Q A B.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: @Col Tn Q A B *)
    apply (col_transitivity_1 Q P A B);Col.
Qed.

(** Unicity of intersection *)

Lemma l6_21 : forall A B C D P Q,
  ~ Col A B C -> C<>D -> Col A B P -> Col A B Q -> Col C D P -> Col C D Q -> P=Q.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    elim (eq_dec_points P Q); intro; try assumption.
(* Goal: @eq (@Tpoint Tn) P Q *)
    cut False.
(* Goal: False *)
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      intro; intuition.
(* Goal: False *)
    apply not_col_distincts in H.
(* Goal: False *)
    spliter.
(* Goal: False *)
    assert (Col C P Q) by (apply col_transitivity_1 with D; Col).
(* Goal: False *)
    assert (Col Q B C).
(* Goal: @Col Tn A B C *)
(* Goal: False *)
      induction (eq_dec_points Q A).
(* Goal: @Col Tn Q B C *)
(* Goal: @Col Tn Q B C *)
(* Goal: False *)
        subst; apply col_transitivity_1 with P; Col.
(* Goal: @Col Tn Q B C *)
(* Goal: False *)
      apply col_transitivity_1 with P; try Col; apply col_permutation_1; apply col_transitivity_1 with A; Col.
(* Goal: False *)
    assert (Col A B C).
(* Goal: @Col Tn A B C *)
(* Goal: False *)
      induction (eq_dec_points Q A).
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        subst Q; assumption.
(* Goal: @Col Tn A B C *)
(* Goal: False *)
      induction (eq_dec_points Q B).
(* Goal: @Col Tn A B C *)
(* Goal: @Col Tn A B C *)
(* Goal: False *)
        subst; apply col_permutation_2; apply col_transitivity_1 with P; try Col.
(* Goal: @Col Tn A B C *)
(* Goal: False *)
      apply col_permutation_2; apply col_transitivity_1 with Q; try Col.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
    contradiction.
Qed.

End T6_1.

Hint Resolve col_transitivity_1 col_transitivity_2 out_col : col.

Section T6_2.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

(* This is l6_25 of Tarski *)
Lemma not_col_exists : forall A B,
 A<>B -> exists C, ~ Col A B C.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
    assert (T:=lower_dim_ex).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
    induction T.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
    induction H0.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
    induction H0.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
    induction (col_dec A B x).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
      induction(col_dec A B x0).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
        induction(col_dec A B x1).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
          induction (eq_dec_points A x).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
            assert (~(Col x x0 x1)) by (unfold Col; auto).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
            treat_equalities; eCol.
          assert (Col A x x0)  by eCol.
          assert (Col A x x1)  by eCol.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
          assert (Col A x0 x1) by eCol.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
          assert (Col x x0 x1) by eCol.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
          contradiction.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        exists x1; assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      exists x0; assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    exists x; assumption.
Qed.

(*
Lemma t2_8 : forall A B C D E : Tpoint,
 Bet A B C -> Bet D B E -> Cong A B D B -> Cong B C B E -> Cong A E C D.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
    induction (eq_dec_points A B); try (treat_equalities; Cong).
    assert (Cong A B D B -> Cong B C B E -> Cong A D D A -> Cong B D B A -> Bet A B C -> Bet D B E -> A <> B -> Cong C D E A).
      apply five_segment.
    apply cong_symmetry.
    apply cong_right_commutativity.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    apply H4; Cong; Between.
Qed.
*)

Lemma col3 : forall X Y A B C,
 X <> Y ->
 Col X Y A -> Col X Y B -> Col X Y C ->
 Col A B C.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: @Col Tn A B C *)
    assert (Col X A B) by (apply col_transitivity_1 with Y; assumption).
(* Goal: @Col Tn A B C *)
    induction(eq_dec_points C X).
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      subst X; apply col_permutation_1; assumption.
(* Goal: @Col Tn A B C *)
    apply col_permutation_1.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    apply col_transitivity_1 with X; try assumption.
(* Goal: @Col Tn C X B *)
      apply col_permutation_2.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      apply col_transitivity_1 with Y; assumption.
(* Goal: @Col Tn C X B *)
    apply col_permutation_2.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    apply col_transitivity_1 with Y; assumption.
Qed.

Lemma colx : forall A B C X Y, A <> B -> Col X Y A -> Col X Y B -> Col A B C -> Col X Y C.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: @Col Tn X Y C *)
    destruct (eq_dec_points X Y).
(* Goal: @Col Tn X Y C *)
(* Goal: @Col Tn X Y C *)
      subst; Col.
(* Goal: @Col Tn A B C *)
    apply (col3 A B); auto; apply col_permutation_1.
(* Goal: @Col Tn X A B *)
(* Goal: @Col Tn Y A B *)
      apply col_transitivity_1 with Y; Col.
(* Goal: @Col Tn Y A B *)
      apply (col_transitivity_2 X); Col.
Qed.

Lemma out2__bet : forall A B C, Out A B C -> Out C A B -> Bet A B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Out Tn A B C) (_ : @Out Tn C A B), @Bet Tn A B C *)
    intros A B C Hout1 Hout2.
(* Goal: @Bet Tn A B C *)
    apply l6_4_1 in Hout2.
(* Goal: @Bet Tn A B C *)
    destruct Hout2 as [_ Hout2].
(* Goal: @Bet Tn A B C *)
    destruct Hout1 as [_ [_ [|]]].
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    assumption.
(* Goal: @Bet Tn A B C *)
    exfalso.
(* Goal: False *)
    apply Hout2.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    assumption.
Qed.

Lemma bet2_le2__le1346 : forall A B C A' B' C', Bet A B C -> Bet A' B' C' -> Le
 A B A' B' -> Le
 B C B' C' ->
  Le
 A C A' C'.
Proof.
  intros A B C A' B' C' HBet HBet' HleAB HleBC.

(* Goal: @Le Tn B' C' B C *)
  elim(eq_dec_points A B).
(* Goal: @Bet Tn A B0 C0 *)
(* Goal: @Le Tn B' C' B C *)
  { intro.
(* Goal: False *)
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    subst B.
    apply (le_transitivity _ _ B' C'); auto.
(* Goal: @Le Tn A' B' A B *)
    apply le_comm.
    exists B'.
    split; Between; Cong.
  }
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
  intro.
  elim(eq_dec_points B C).
(* Goal: @Bet Tn A B0 C0 *)
(* Goal: @Le Tn B' C' B C *)
  { intro.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    subst C.
    apply (le_transitivity _ _ A' B'); auto.
    exists B'; Cong.
  }
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
  intro.

  assert(A' <> B') by (intro; subst B'; assert(A = B); auto; apply (le_zero _ _ A'); auto).
  assert(B' <> C') by (intro; subst C'; assert(B = C); auto; apply (le_zero _ _ B'); auto).
  destruct HleAB as [B0 []].
  assert(A' <> B0) by (intro; subst B0; assert(A = B); auto; apply (cong_reverse_identity A'); Cong).
  assert(HC0 := segment_construction A' B0 B C).
  destruct HC0 as [C0 []].
  assert(B0 <> C0) by (intro; subst C0; assert(B = C); auto; apply (cong_reverse_identity B0); auto).
  exists C0.
(* Goal: and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C)) *)
  split.
  2: apply (l2_11 _ B _ _ B0); Cong.
  apply (outer_transitivity_between2 _ B0); auto.
  assert(Bet B0 B' C') by (apply between_symmetry; apply (between_inner_transitivity _ _ _ A'); Between).
(* Goal: @Bet Tn A B0 C0 *)
  apply l6_13_1.
  - elim(eq_dec_points B0 B').
(* Goal: @Bet Tn A B0 C0 *)
(* Goal: @Le Tn B' C' B C *)
    { intro.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      subst.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      apply (l6_2 _ _ A'); Between.
    }
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    intro.
    apply (l6_7 _ _ B').
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    apply (l6_2 _ _ A'); Between.
    apply bet_out; auto.
  - apply (le_transitivity _ _ B' C').
      apply (l5_6 B C B' C'); Cong.
(* Goal: @Le Tn A' B' A B *)
      apply le_comm.
      exists B'.
      split; Between; Cong.
Qed.

Lemma bet2_le2__le2356 : forall A B C A' B' C', Bet A B C -> Bet A' B' C' ->
  Le A B A' B' -> Le A' C' A C -> Le 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') (_ : @Le Tn A B A' B') (_ : @Le Tn A' C' A C), @Le Tn B' C' B C *)
  intros A B C A' B' C' HBet HBet' HLe1 HLe2.
(* Goal: @Le Tn B' C' B C *)
  elim(eq_dec_points A B).
(* Goal: @Bet Tn A B0 C0 *)
(* Goal: @Le Tn B' C' B C *)
  { intro; treat_equalities.
(* Goal: @Le Tn B' C' A C *)
    apply (le_transitivity _ _ A' C'); auto.
(* Goal: @Le Tn A' B' A' C' *)
    destruct (l5_12_a A' B' C'); auto.
  }
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
  intro.
(* Goal: @Le Tn B' C' B C *)
  assert (A<>C) by (intro; treat_equalities; auto).
(* Goal: @Le Tn B' C' B C *)
  destruct (l5_5_1 A B A' B' HLe1) as [B0 [HBet1 HCong1]].
(* Goal: @Le Tn B' C' B C *)
  assert (A<>B0) by (intro; treat_equalities; auto).
(* Goal: @Le Tn B' C' B C *)
  destruct HLe2 as [C0 [HBet2 HCong2]].
(* Goal: @Le Tn B' C' B C *)
    assert (A<>C0) by (intro; treat_equalities; auto).
(* Goal: @Le Tn B' C' B C *)
  assert (Bet A B0 C0).
(* Goal: @Bet Tn A B0 C0 *)
(* Goal: @Le Tn B' C' B C *)
  { apply l6_13_1.
      apply (l6_7 _ _ B); [|apply (l6_7 _ _ C)]; [apply l6_6| |apply l6_6]; apply bet_out; auto.
(* Goal: @Le Tn A B0 A C0 *)
    apply (l5_6 A' B' A' C'); Cong.
(* Goal: @Le Tn A' B' A' C' *)
    destruct (l5_12_a A' B' C'); auto.
  }
(* Goal: @Le Tn B' C' B C *)
  apply (l5_6 B0 C0 B C); Cong; [apply (le_transitivity _ _ B C0)|].
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    destruct (l5_12_a B B0 C0); eBetween.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    destruct (l5_12_a B C0 C); eBetween.
(* Goal: @Cong Tn B0 C0 B' C' *)
    apply cong_commutativity; apply (l4_3 _ _ A _ _ A'); Between; Cong.
Qed.

Lemma bet2_le2__le1245 : forall A B C A' B' C', Bet A B C -> Bet A' B' C' ->
  Le B C B' C' -> Le A' C' A C -> Le A' B' A B.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
  intros A B C A' B' C'; intros.
(* Goal: @Le Tn A' B' A B *)
  apply le_comm.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
  apply (bet2_le2__le2356 C _ _ C'); Le; Between.
Qed.

Lemma cong_preserves_bet : forall B A' A0 E D' D0,
  Bet B A' A0 -> Cong B A' E D' -> Cong B A0 E D0 -> Out E D' D0 ->
  Bet E D' D0.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
    unfold Out in H2.
(* Goal: False *)
    spliter.
    induction H4.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
    assert (Le
 E D0 E D').
      eapply l5_5_2.
      exists D'.
(* Goal: and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C)) *)
      split.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        assumption.
      Cong.
    assert(Le
 E D' E D0).
      eapply l5_6.
(* Goal: and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C)) *)
      repeat split.
        2:apply H0.
        2:apply H1.
      eapply l5_5_2.
      exists A0.
(* Goal: and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C)) *)
      split.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        assumption.
      Cong.
    assert(Cong E D' E D0).
      apply le_anti_symmetry.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
    assert(D0 = D').
      eapply between_cong.
        apply H4.
      Cong.
    subst D'.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    Between.
Qed.

Lemma out_cong_cong : forall B A A0 E D D0,
 Out B A A0 -> Out E D D0 ->
 Cong B A E D -> Cong B A0 E D0 ->
 Cong A A0 D D0.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: or (@Bet Tn A B C) (or (@Bet Tn B C A) (@Bet Tn C A B)) *)
    unfold Out in H.
(* Goal: False *)
    spliter.
    induction H4.
      assert (Bet E D D0).
        eapply cong_preserves_bet.
          2:apply H1.
          2:apply H2.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
          assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        assumption.
      apply cong_commutativity.
      eapply l4_3.
        apply between_symmetry.
        apply H4.
        apply between_symmetry.
        apply H5.
        Cong.
      Cong.
    assert (Bet E D0 D).
      eapply cong_preserves_bet.
        2:apply H2.
        2:apply H1.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        assumption.
      apply l6_6.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
    eapply l4_3;eBetween;Cong.
Qed.

Lemma not_out_bet : forall A B C, Col A B C -> ~ Out B A C -> Bet A B C.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: @Bet Tn A B C *)
    unfold Out in H0.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    induction (eq_dec_points A B).
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      subst.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      Between.
(* Goal: @Bet Tn A B C *)
    induction (eq_dec_points B C).
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      subst.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      Between.
(* Goal: @Bet Tn A B C *)
    unfold Col in *.
(* Goal: @Bet Tn A B C *)
    decompose [or] H;clear H.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
(* Goal: @Bet Tn A B C *)
      exfalso.
(* Goal: False *)
      apply H0.
(* Goal: False *)
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      intuition.
(* Goal: @Bet Tn A B C *)
    exfalso.
(* Goal: False *)
    apply H0.
(* Goal: False *)
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    intuition.
Qed.

Lemma or_bet_out : forall A B C, Bet A B C \/ Out B A C \/ ~Col A B C.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: or (@Bet Tn A B C) (or (@Out Tn B A C) (not (@Col Tn A B C))) *)
    destruct (col_dec A B C); auto.
(* Goal: or (@Bet Tn A B C) (or (@Out Tn B A C) (not (@Col Tn A B C))) *)
    destruct (out_dec B A C); auto.
(* Goal: or (@Bet Tn A B C) (or (@Out Tn B A C) (not (@Col Tn A B C))) *)
    left; apply not_out_bet; trivial.
Qed.

Lemma not_bet_out : forall A B C,
 Col A B C -> ~Bet A B C -> Out B A C.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
    destruct (or_bet_out A B C) as [HBet|[HOut|HNCol]]; trivial; contradiction.
Qed.

Lemma not_bet_and_out :
 forall A B C,
 ~ (Bet A B C /\ Out B A C).
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    intro.
(* Goal: False *)
    spliter.
(* Goal: @Bet Tn A B C *)
    unfold Out in H0.
(* Goal: False *)
    spliter.
    induction H2.
      assert ( A = B).
        eapply between_equality.
          apply H.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        assumption.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
      contradiction.
    assert(C = B).
      eapply between_equality.
        apply between_symmetry.
        apply H.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
    contradiction.
Qed.

Lemma out_to_bet :
 forall A B C A' B' C',
  Col A' B' C' ->
 (Out B A C <-> Out B' A' C') ->
  Bet A B C ->
  Bet A' B' C'.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
    induction(out_dec B A C).
      unfold Out in H2.
(* Goal: False *)
      spliter.
      induction H4.
        assert( A = B).
          eapply between_equality.
            apply H1.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
          assumption.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
        contradiction.
      assert(C = B).
        apply(between_symmetry) in H4.
        eapply between_equality.
          apply between_symmetry.
          apply H1.
        apply between_symmetry.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        assumption.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn A B C)) *)
      contradiction.
    destruct H0.
    assert (~Out B' A' C').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      intro.
      apply H2.
      apply H3.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
    apply not_out_bet.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    assumption.
Qed.

Lemma col_out2_col  : forall A B C AA CC, Col A B C -> Out B A AA -> Out B C CC -> Col AA B CC.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
    induction H.
      assert (Bet AA B CC).
        eapply bet_out_out_bet.
          apply H.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
          assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        assumption.
(* Goal: @Col Tn X P S *)
      unfold Col.
      left.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
    induction H.
      assert(Out B AA CC).
        eapply l6_7.
          eapply l6_6.
(* Goal: False *)
          apply H0.
        apply l6_6.
        eapply l6_7.
          apply l6_6.
          apply H1.
        apply bet_out.
(* Goal: and (@Out Tn B A P) (@Out Tn B C P) *)
          unfold Out in *.
(* Goal: False *)
          spliter.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
          assumption.
(* Goal: and (@Out Tn B A P) (@Out Tn B C P) *)
          unfold Out in *.
(* Goal: False *)
          spliter.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
          assumption.
      apply col_permutation_4.
      apply out_col.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
    assert(Out B AA CC).
      eapply l6_6.
      eapply l6_7.
        eapply l6_6.
        apply H1.
      eapply l6_6.
      eapply l6_7.
        eapply l6_6.
(* Goal: False *)
        apply H0.
      apply bet_out.
(* Goal: and (@Out Tn B A P) (@Out Tn B C P) *)
        unfold Out in *.
(* Goal: False *)
        spliter.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        assumption.
(* Goal: and (@Out Tn B A P) (@Out Tn B C P) *)
        unfold Out in *.
(* Goal: False *)
        spliter.
      apply between_symmetry.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
    apply col_permutation_4.
    apply out_col.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    assumption.
Qed.

Lemma bet2_out_out : forall A B C B' C', B <> A -> B' <> A -> Out A C C' -> Bet A B C -> Bet A B' C' -> Out A B B'.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
    induction(eq_dec_points B' C').
      subst C'.
(* Goal: and (@Out Tn B A P) (@Out Tn B C P) *)
      unfold Out in *.
(* Goal: False *)
      spliter.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      repeat split; try assumption.
      induction H5.
        left.
        eapply between_exchange4.
          apply H2.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        assumption.
      eapply l5_3.
        apply H2.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
(* Goal: and (@Out Tn B A P) (@Out Tn B C P) *)
    unfold Out in *.
(* Goal: False *)
    spliter.
(* Goal: and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C)) *)
    repeat split.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
    induction H6.
      assert(Bet A B C').
        eapply between_exchange4.
          apply H2.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        assumption.
      eapply l5_3.
        apply H7.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
    assert(Bet B' C' C).
      eapply between_exchange3.
        apply H3.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
    assert(Bet A B' C).
      eapply outer_transitivity_between.
        apply H3.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
    eapply l5_3.
      apply H2.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    assumption.
Qed.

Lemma bet2__out : forall A B C B', A <> B -> A <> B' -> Bet A B C -> Bet A B' C -> Out A B B'.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: @Out Tn A B B' *)
    apply bet2_out_out with C C; auto.
(* Goal: @Out Tn A C C *)
    apply bet_neq12__neq in H1; auto.
(* Goal: @Out Tn A C C *)
    apply out_trivial; auto.
Qed.

Lemma out2_out_1 : forall B C D X,
 Out B X C -> Out B X D -> Out B C D.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: and (@Out Tn B A P) (@Out Tn B C P) *)
    unfold Out in *.
(* Goal: False *)
    spliter.
(* Goal: and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C)) *)
    repeat split.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
    induction H2; induction H4.
      eapply l5_1.
        2: apply H4.
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
        auto.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
      left.
      eapply between_exchange4.
        apply H4.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
      right.
      eapply between_exchange4.
        apply H2.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
    eapply l5_3.
      apply H4.
    apply H2.
Qed.

Lemma out2_out_2 : forall B C D X,
 Out B C X -> Out B D X -> Out B C D.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
    eapply out2_out_1.
      apply l6_6.
      apply H.
    apply l6_6.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    assumption.
Qed.

Lemma out_bet_out_1 : forall A B C P,
 Out P A C -> Bet A B C -> Out P A B.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
    induction (eq_dec_points B P).
      subst P.
      apply False_ind.
      apply (not_bet_and_out A B C).
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      split; assumption.
(* Goal: and (@Out Tn B A P) (@Out Tn B C P) *)
    unfold Out in *.
(* Goal: False *)
    spliter.
(* Goal: and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C)) *)
    repeat split.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
    induction H3.
      left.
      eapply between_inner_transitivity.
        apply H3.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
    right.
    eapply between_exchange2.
      apply H3.
    apply between_symmetry.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    assumption.
Qed.

Lemma out_bet_out_2 : forall A B C P,
 Out P A C -> Bet A B C -> Out P B C.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
    apply l6_6.
    eapply out_bet_out_1.
      apply l6_6.
      apply H.
    apply between_symmetry.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    assumption.
Qed.

Lemma out_bet__out : forall A B P Q,
 Bet P Q A -> Out Q A B -> Out P A B.
Proof.
(* Goal: forall (A B P Q : @Tpoint Tn) (_ : @Bet Tn P Q A) (_ : @Out Tn Q A B), @Out Tn P A B *)
    intros A B P Q HBet Hout.
    destruct Hout as [HAQ [HBQ [HQAB|HQBA]]]; [|apply l6_6];
(* Goal: not (@eq (@Tpoint Tn) C A) *)
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@Bet Tn A B' C) (@Cong Tn C B' A B)) *)
      apply bet_out; eBetween; intro; treat_equalities; auto.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    apply HBQ; apply (between_equality _ _ A); Between.
Qed.

Lemma segment_reverse : forall A B C, Bet A B C -> exists B', Bet A B' C /\ Cong C B' A B.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
  intros.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@Bet Tn A B' C) (@Cong Tn C B' A B)) *)
  destruct (eq_dec_points A B).
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@Bet Tn A B' C) (@Cong Tn C B' A B)) *)
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@Bet Tn A B' C) (@Cong Tn C B' A B)) *)
    subst B; exists C; finish.
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
  destruct (segment_construction_3 C A A B) as [B' []]; auto.
(* Goal: not (@eq (@Tpoint Tn) C A) *)
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@Bet Tn A B' C) (@Cong Tn C B' A B)) *)
    intro; treat_equalities; auto.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@Bet Tn A B' C) (@Cong Tn C B' A B)) *)
  exists B'; split; trivial.
  apply between_symmetry, (cong_preserves_bet A B C); Cong.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
  apply l6_6; assumption.
Qed.

Lemma diff_col_ex : forall A B, exists C, A <> C /\ B <> C /\ Col A B C.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    assert (exists C, Bet A B C /\ B <> C).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Bet Tn A B C) (not (@eq (@Tpoint Tn) B C))) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
      apply point_construction_different.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    ex_and H C.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    exists C.
(* Goal: and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C)) *)
    split.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      intro.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      induction (eq_dec_points A B).
(* Goal: False *)
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
        subst B.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
        subst C.
(* Goal: False *)
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
        intuition.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      subst C.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      Between.
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    assert_cols.
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    auto.
Qed.

Lemma diff_bet_ex3 : forall A B C,
 Bet A B C ->
 exists D, A <> D /\ B <> D /\ C <> D /\ Col A B D.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
    induction (eq_dec_points A B).
(* Goal: @Bet Tn A B C *)
      induction (eq_dec_points B C).
        assert (exists D, Bet B C D /\ C <> D).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Bet Tn A B C) (not (@eq (@Tpoint Tn) B C))) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
          apply point_construction_different.
        ex_and H2 D.
        exists D.
(* Goal: and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C)) *)
        repeat split.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
          subst C.
          subst A.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
          assumption.
          subst A.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
          subst C.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
          assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
          assumption.
(* Goal: @Col Tn X P S *)
        unfold Col.
        left.
        subst A.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
        subst C.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        assumption.
      assert (exists D, Bet B C D /\ C <> D).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Bet Tn A B C) (not (@eq (@Tpoint Tn) B C))) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
        apply point_construction_different.
      ex_and H2 D.
      exists D.
(* Goal: and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C)) *)
      repeat split.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
        intro.
        subst D.
        apply between_symmetry in H.
        apply H1.
        eapply between_equality.
          apply H2.
        apply H.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
        intro.
        subst D.
        subst A.
        apply between_identity in H2.
        apply H3.
(* Goal: False *)
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
        subst B.
        reflexivity.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        assumption.
(* Goal: @Col Tn X P S *)
      unfold Col.
      left.
      eapply outer_transitivity_between.
        apply H.
        apply H2.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
(* Goal: @Bet Tn A B C *)
    induction (eq_dec_points B C).
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      subst C.
      cut(exists D : Tpoint, A <> D /\ B <> D /\ Col A B D).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
        intro.
        ex_and H1 D.
        exists D.
(* Goal: and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C)) *)
        repeat split.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
          assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
          assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
          assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        assumption.
      apply diff_col_ex.
    assert (exists D, Bet B C D /\ C <> D).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Bet Tn A B C) (not (@eq (@Tpoint Tn) B C))) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
      apply point_construction_different.
    ex_and H2 D.
    exists D.
(* Goal: and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C)) *)
    repeat split.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      intro.
      subst D.
      assert (B = C).
        eapply between_equality.
          apply H2.
        apply between_symmetry.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        assumption.
      apply H1.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      intro.
      subst D.
      apply between_identity in H2.
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      subst C.
      apply H1.
      reflexivity.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
(* Goal: @Col Tn X P S *)
    unfold Col.
    left.
    eapply outer_transitivity_between.
      apply H.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    assumption.
Qed.

Lemma diff_col_ex3 : forall A B C,
 Col A B C -> exists D, A <> D /\ B <> D /\ C <> D /\ Col A B D.
Proof.
(* Goal: forall A B : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C))) *)
    intros.
    assert(cas1 := diff_bet_ex3 A B C).
    assert(cas2 := diff_bet_ex3 B C A).
    assert(cas3 := diff_bet_ex3 C A B).
    unfold Col in H.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
    induction H.
      apply (diff_bet_ex3 A B C).
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
    induction H.
      assert (HH:=H).
(* Goal: @Bet Tn A B C *)
      induction (eq_dec_points B C).
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
        subst C.
        assert (exists C, A <> C /\ B <> C /\ Col A B C).
          apply (diff_col_ex).
        ex_and H0 D.
        exists D.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        repeat split; assumption.
      apply cas2 in HH.
      ex_and HH D.
      exists D.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      repeat split; try assumption.
(* Goal: @Col Tn C X B *)
      apply col_permutation_2.
      eapply col_transitivity_1.
(* Goal: False *)
        apply H0.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
        assumption.
(* Goal: @Col Tn X P S *)
      unfold Col.
      left.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
    induction (eq_dec_points A C).
(* Goal: False *)
(* Goal: and (not (@eq (@Tpoint Tn) B C)) (@Col Tn A B C) *)
      subst C.
      assert (exists C, A <> C /\ B <> C /\ Col A B C).
        apply (diff_col_ex).
      ex_and H0 D.
      exists D.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      repeat split; assumption.
    assert (HH:=H).
    apply cas3 in HH.
    ex_and HH D.
    exists D.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    repeat split; try assumption.
    apply col_permutation_5.
    eapply col_transitivity_1.
(* Goal: False *)
      apply H0.
      apply col_permutation_4.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
      assumption.
(* Goal: @Col Tn X P S *)
    unfold Col.
    right;right.
    apply between_symmetry.
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    assumption.
Qed.

End T6_2.

Hint Resolve bet_out out_trivial l6_6 : out.