Require Export GeoCoq.Tarski_dev.Ch09_plane.

Section Upper_dim.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Definition upper_dim_axiom := forall A B C P Q : Tpoint,
  P <> Q -> Cong A P A Q -> Cong B P B Q -> Cong C P C Q ->
  (Bet A B C \/ Bet B C A \/ Bet C A B).

Definition all_coplanar_axiom := forall A B C D, Coplanar A B C D.

Lemma upper_dim_implies_per2__col :
  upper_dim_axiom ->
  (forall A B C X, Per A X C -> X <> C -> Per B X C -> Col A B X).
Proof.
(* Goal: forall (_ : upper_dim_axiom) (A B C X : @Tpoint Tn) (_ : @Per Tn A X C) (_ : not (@eq (@Tpoint Tn) X C)) (_ : @Per Tn B X C), @Col Tn A B X *)
intros HUD A B C X HPer1 HDiff HPer2.
(* Goal: @Col Tn A B X *)
destruct HPer1 as [C' HPer1].
(* Goal: @Col Tn A B X *)
destruct HPer2 as [C'' HPer2].
(* Goal: @Col Tn A B X *)
assert (C' = C'') by (apply symmetric_point_uniqueness with C X; spliter; auto); treat_equalities.
(* Goal: @Col Tn A B X *)
unfold upper_dim_axiom in HUD.
(* Goal: @Col Tn A B X *)
spliter; assert_diffs; unfold Midpoint in *; spliter; apply HUD with C C'; Cong.
Qed.

Lemma upper_dim_implies_col_perp2__col :
  upper_dim_axiom ->
  (forall A B X Y P,
   Col A B P ->
   Perp A B X P ->
   Perp P A Y P ->
   Col Y X P).
Proof.
intro HUP; intros.
assert (P <> A).
eapply perp_not_eq_1.
(* Goal: False *)
(* Goal: @OS Tn A B X Y *)
apply H1.
eapply upper_dim_implies_per2__col; auto.
apply perp_in_per.
apply perp_in_sym.
apply perp_perp_in.
(* Goal: False *)
(* Goal: @OS Tn A B X Y *)
apply H1.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
assumption.
apply perp_in_per.
apply perp_in_sym.
apply perp_perp_in.
(* Goal: @Perp Tn B A X A *)
(* Goal: @Col Tn B A A *)
(* Goal: not (@Col Tn X B A) *)
(* Goal: not (@Col Tn Y B A) *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
apply perp_left_comm.
eapply perp_col.
auto.
(* Goal: False *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
apply H0.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
assumption.
Qed.

Lemma upper_dim_implies_perp2__col :
  upper_dim_axiom ->
  (forall X Y Z A B,
   Perp X Y A B ->
   Perp X Z A B ->
   Col X Y Z).
Proof.
intro HUP; intros.
induction(col_dec A B X).
  induction(eq_dec_points X A).
    subst A.
    assert(X <> B).
      apply perp_distinct in H.
      spliter.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
      assumption.
    apply perp_right_comm in H.
    apply perp_perp_in in H.
    apply perp_in_comm in H.
    apply perp_in_per in H.
    apply perp_right_comm in H0.
    apply perp_perp_in in H0.
    apply perp_in_comm in H0.
    apply perp_in_per in H0.
(* Goal: @Col Tn X A B *)
(* Goal: @OS Tn A B X Y *)
    apply col_permutation_2.
    eapply (upper_dim_implies_per2__col).
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
      assumption.
(* Goal: False *)
(* Goal: not (@Col Tn Y B A) *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
      apply H.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
      assumption.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
    assumption.
  assert(Perp A X X Y ).
    eapply perp_col.
      auto.
      apply perp_sym.
(* Goal: False *)
(* Goal: not (@Col Tn Y B A) *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
      apply H.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
    assumption.
  assert(Perp A X X Z).
    eapply perp_col.
      auto.
      apply perp_sym.
(* Goal: False *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
      apply H0.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
    assumption.
(* Goal: @Col Tn X A B *)
(* Goal: @OS Tn A B X Y *)
  apply col_permutation_2.
  apply upper_dim_implies_per2__col with A.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
    assumption.
    apply perp_in_per.
    apply perp_in_comm.
    apply perp_perp_in.
    apply perp_sym.
    eapply perp_col.
      auto.
      apply perp_sym.
(* Goal: False *)
(* Goal: not (@Col Tn Y B A) *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
      apply H.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
    assumption.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
    assumption.
  apply perp_in_per.
  apply perp_in_comm.
  apply perp_perp_in.
  apply perp_sym.
  eapply perp_col.
    auto.
    apply perp_sym.
(* Goal: False *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
    apply H0.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
  assumption.
assert(HH0:=H).
assert(HH1:=H0).
unfold Perp in H.
unfold Perp in H0.
ex_and H Y0.
ex_and H0 Z0.
assert(HH2:=H).
assert(HH3:=H2).
apply perp_in_col in H.
apply perp_in_col in H2.
spliter.
assert(Perp X Y0 A B).
  eapply perp_col.
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
    intro.
    subst Y0.
(* Goal: @TS Tn A B X Y *)
    contradiction.
    apply HH0.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
  assumption.
assert(Perp X Z0 A B).
  eapply perp_col.
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
    intro.
    subst Z0.
(* Goal: @TS Tn A B X Y *)
    contradiction.
    apply HH1.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
  assumption.
assert(Y0 = Z0).
  eapply l8_18_uniqueness.
(* Goal: False *)
(* Goal: @OS Tn A B X Y *)
    apply H1.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
    assumption.
    apply perp_sym.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
    assumption.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
    assumption.
  apply perp_sym.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
  assumption.
subst Z0.
eapply (col_transitivity_1 _ Y0).
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
  intro.
  subst Y0.
(* Goal: @TS Tn A B X Y *)
  contradiction.
(* Goal: @Col Tn Y A B *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
  Col.
(* Goal: @Col Tn Y A B *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
Col.
Qed.

Lemma upper_dim_implies_not_two_sides_one_side_aux :
  upper_dim_axiom ->
  (forall A B X Y PX,
   A <> B -> PX <> A ->
   Perp A B X PX ->
   Col A B PX ->
   ~ Col X A B ->
   ~ Col Y A B ->
   ~ TS A B X Y ->
   OS A B X Y).
Proof.
(* Goal: forall (_ : upper_dim_axiom) (A B X Y : @Tpoint Tn) (_ : not (@Col Tn X A B)) (_ : not (@Col Tn Y A B)), or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
intro HUD; intros.
assert(exists P, exists T, Perp PX A P PX /\ Col PX A T /\ Bet Y T P).
apply l8_21.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
assumption.
ex_elim H6 P.
ex_and H7 T.
assert(HH:= upper_dim_implies_col_perp2__col HUD A B X P PX H2 H1 H6).
assert(~Col P A B).
apply perp_not_col in H6.
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
intro.
apply H6.
ColR.
assert(TS PX A P Y).
repeat split.
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
intro.
apply H9.
ColR.
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
intro.
apply H4.
ColR.
exists T.
split.
(* Goal: @Col Tn X A B *)
(* Goal: @OS Tn A B X Y *)
apply col_permutation_2.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
assumption.
apply between_symmetry.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
assumption.
assert(X <> PX).
apply perp_not_eq_2 in H1.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
assumption.
assert(P <> PX).
apply perp_not_eq_2 in H6.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
assumption.
assert(HA:= (or_bet_out X PX P)).
induction HA.
assert(TS PX A P X).
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
repeat split; try assumption.
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
intro.
apply H9.
ColR.
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
intro.
apply H3.
ColR.
exists PX.
split.
apply col_trivial_1.
apply between_symmetry.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
assumption.
eapply l9_8_1.
apply l9_2.
eapply (col_two_sides _ PX).
apply col_permutation_5.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
assumption.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
assumption.
(* Goal: @TS Tn A B X Y *)
(* Goal: @OS Tn A B X Y *)
apply invert_two_sides.
apply H14.
eapply (col_two_sides _ PX).
apply col_permutation_5.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
assumption.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
assumption.
(* Goal: @TS Tn A B X Y *)
(* Goal: @OS Tn A B X Y *)
apply invert_two_sides.
apply l9_2.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
assumption.
induction H13.
assert(TS A B P Y).
eapply (col_two_sides _ PX).
(* Goal: @Col Tn Y A B *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
Col.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
assumption.
apply  invert_two_sides.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
assumption.
assert(HO:= out_two_sides_two_sides A B X Y P PX (sym_not_eq H0) H2 H13 H14).
(* Goal: @TS Tn A B X Y *)
contradiction.
apply col_permutation_1 in HH.
(* Goal: @TS Tn A B X Y *)
contradiction.
Qed.

Lemma upper_dim_implies_not_two_sides_one_side :
  upper_dim_axiom ->
  (forall A B X Y,
   ~ Col X A B ->
   ~ Col Y A B ->
   ~ TS A B X Y ->
   OS A B X Y).
Proof.
(* Goal: forall (_ : upper_dim_axiom) (A B X Y : @Tpoint Tn) (_ : not (@Col Tn X A B)) (_ : not (@Col Tn Y A B)), or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
    intro HUD; intros.
(* Goal: @OS Tn A B X Y *)
    assert (A <> B) by (intro; subst; Col).
(* Goal: @OS Tn A B X Y *)
    assert(exists PX, Col A B PX /\ Perp A B X PX).
(* Goal: @ex (@Tpoint Tn) (fun PX : @Tpoint Tn => and (@Col Tn A B PX) (@Perp Tn A B X PX)) *)
(* Goal: @OS Tn A B X Y *)
      apply l8_18_existence.
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
      intro.
(* Goal: False *)
(* Goal: not (@Col Tn Y B A) *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
      apply H.
(* Goal: @Col Tn X A B *)
(* Goal: @OS Tn A B X Y *)
      apply col_permutation_2.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
      assumption.
(* Goal: @OS Tn A B X Y *)
    ex_and H3 PX.
(* Goal: @OS Tn A B X Y *)
    induction(eq_dec_points PX A).
(* Goal: @OS Tn A B X Y *)
(* Goal: @OS Tn A B X Y *)
      subst PX.
(* Goal: @OS Tn A B X Y *)
(* Goal: @OS Tn A B X Y *)
      apply invert_one_side.
      eapply (upper_dim_implies_not_two_sides_one_side_aux HUD _ _ _ _ A); auto.
(* Goal: @Perp Tn B A X A *)
(* Goal: @Col Tn B A A *)
(* Goal: not (@Col Tn X B A) *)
(* Goal: not (@Col Tn Y B A) *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
        apply perp_left_comm.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
        assumption.
(* Goal: @Col Tn Y A B *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
        Col.
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
        intro.
(* Goal: False *)
(* Goal: not (@Col Tn Y B A) *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
        apply H.
(* Goal: @Col Tn Y A B *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
        Col.
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
        intro.
(* Goal: False *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
        apply H0.
(* Goal: @Col Tn Y A B *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
        Col.
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
      intro.
(* Goal: False *)
(* Goal: @OS Tn A B X Y *)
      apply H1.
(* Goal: @TS Tn A B X Y *)
(* Goal: @OS Tn A B X Y *)
      apply invert_two_sides.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
      assumption.
    apply (upper_dim_implies_not_two_sides_one_side_aux HUD _ _ _ _ PX); auto.
Qed.

Lemma upper_dim_implies_not_one_side_two_sides :
  upper_dim_axiom ->
  (forall A B X Y,
   ~ Col X A B ->
   ~ Col Y A B ->
   ~ OS A B X Y ->
   TS A B X Y).
Proof.
(* Goal: forall (_ : upper_dim_axiom) (A B X Y : @Tpoint Tn) (_ : not (@Col Tn X A B)) (_ : not (@Col Tn Y A B)), or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
    intro HUD; intros.
(* Goal: @TS Tn A B X Y *)
    intros.
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
    induction(two_sides_dec A B X Y).
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
      assumption.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
    apply upper_dim_implies_not_two_sides_one_side in H2; try assumption.
(* Goal: @TS Tn A B X Y *)
    contradiction.
Qed.

Lemma upper_dim_implies_one_or_two_sides :
  upper_dim_axiom ->
  (forall A B X Y,
   ~ Col X A B ->
   ~ Col Y A B ->
   TS A B X Y \/ OS A B X Y).
Proof.
(* Goal: forall (_ : upper_dim_axiom) (A B X Y : @Tpoint Tn) (_ : not (@Col Tn X A B)) (_ : not (@Col Tn Y A B)), or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
intro HUD; intros.
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
induction(two_sides_dec A B X Y).
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
left.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
assumption.
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
right.
(* Goal: @TS Tn A B X Y *)
(* Goal: or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
apply upper_dim_implies_not_two_sides_one_side in H1; try assumption.
Qed.

Lemma upper_dim_implies_all_coplanar : upper_dim_axiom -> all_coplanar_axiom.
Proof.
(* Goal: @TS Tn A B X Y *)
intro HUD; unfold all_coplanar_axiom; intros.
elim (col_dec A B C); Cop; intro HABC.
elim (col_dec A B D); Cop; intro HABD.
elim (col_dec A C D); Cop; intro HACD.
elim (upper_dim_implies_one_or_two_sides HUD A B C D); Col;
(* Goal: @Col Tn Y A B *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
elim (upper_dim_implies_one_or_two_sides HUD A C B D); Col.

  {
  intros HTS1 HTS2; destruct HTS1 as [Hc1 [Hc2 [I [HCol HBet]]]].
(* Goal: @Col Tn Y A B *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
  clear Hc1; clear Hc2; exists I; right; left; assert_cols; Col.
  }

  {
  intros HOS HTS; destruct HTS as [Hc1 [Hc2 [I [HCol HBet]]]].
(* Goal: @Col Tn Y A B *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
  clear Hc1; clear Hc2; exists I; left; assert_cols; Col.
  }

  {
  intros HTS HOS; destruct HTS as [Hc1 [Hc2 [I [HCol HBet]]]].
(* Goal: @Col Tn Y A B *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
  clear Hc1; clear Hc2; exists I; right; left; assert_cols; Col.
  }

  {
  intros HOS1 HOS2; destruct (l9_31 A B D C) as [Hc1 [Hc2 [I [HCol HBet]]]];
  try (apply one_side_symmetry; auto); clear Hc1; clear Hc2;
(* Goal: @Col Tn Y A B *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
  exists I; right; right; assert_cols; Col.
  }
Qed.

Lemma all_coplanar_implies_upper_dim : all_coplanar_axiom -> upper_dim_axiom.
Proof.
(* Goal: forall _ : all_coplanar_axiom, upper_dim_axiom *)
intros HAC A B C P Q.
(* Goal: forall (_ : not (@eq (@Tpoint Tn) P Q)) (_ : @Cong Tn A P A Q) (_ : @Cong Tn B P B Q) (_ : @Cong Tn C P C Q), or (@Bet Tn A B C) (or (@Bet Tn B C A) (@Bet Tn C A B)) *)
apply cong3_cop2__col; apply HAC.
Qed.

Lemma all_coplanar_upper_dim : all_coplanar_axiom <-> upper_dim_axiom.
Proof.
split;
try apply all_coplanar_implies_upper_dim;
apply upper_dim_implies_all_coplanar.
Qed.

Lemma upper_dim_stab : ~ ~ upper_dim_axiom -> upper_dim_axiom.
Proof.
(* Goal: forall _ : not (not upper_dim_axiom), upper_dim_axiom *)
  intros nnupper A B C P Q HPQ H1 H2 H3.
  destruct (col_dec A B C) as [|HNCol]; auto.
(* Goal: or (@Bet Tn A B C) (or (@Bet Tn B C A) (@Bet Tn C A B)) *)
  exfalso.
(* Goal: False *)
  apply nnupper.
(* Goal: not upper_dim_axiom *)
  intro upper.
(* Goal: @Col Tn Y A B *)
(* Goal: not (@TS Tn B A X Y) *)
(* Goal: @OS Tn A B X Y *)
  apply HNCol.
  apply upper with P Q; auto.
Qed.

End Upper_dim.