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

Section Upper_dim_3.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

(** In this file, we prove that all the following properties are equivalent. *)

(** If three points A, B and C are equidistant to three distinct points P, Q and R,
    then A, B and C are collinear. *)

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

(** If four points are equidistant to two distinct points, then they are coplanar. *)

Definition median_planes_axiom := forall A B C D P Q, P <> Q ->
  Cong A P A Q -> Cong B P B Q -> Cong C P C Q -> Cong D P D Q ->
  Coplanar A B C D.

(** If two planes meet in some point, then they also meet in another point. *)

Definition plane_intersection_axiom := forall A B C D E F P,
  Coplanar A B C P -> Coplanar D E F P ->
  exists Q, Coplanar A B C Q /\ Coplanar D E F Q /\ P <> Q.

(** If two points do not lie on a plane, then they are either
    on opposite sides or on the same side of the plane. *)

Definition space_separation_axiom := forall A B C P Q,
  ~ Coplanar A B C P -> ~ Coplanar A B C Q -> TSP A B C P Q \/ OSP A B C P Q.

(** The line segments SU1, SU2, SU3 and SU4 can not form an orthonormal family *)

Definition orthonormal_family_axiom := forall S U1' U1 U2 U3 U4,
  ~ (S <> U1' /\ Bet U1 S U1' /\
     Cong S U1 S U1' /\ Cong S U2 S U1' /\ Cong S U3 S U1' /\ Cong S U4 S U1' /\
     Cong U1 U2 U1' U2 /\ Cong U1 U3 U1' U2 /\ Cong U1 U4 U1' U2 /\
     Cong U2 U3 U1' U2 /\ Cong U2 U4 U1' U2 /\ Cong U3 U4 U1' U2).


Lemma upper_dim_3_stab : ~ ~ upper_dim_3_axiom -> upper_dim_3_axiom.
Proof.
(* Goal: forall _ : not (not upper_dim_3_axiom), upper_dim_3_axiom *)
  intros nnupper A B C P Q R; intros.
(* Goal: or (@Bet Tn A B C) (or (@Bet Tn B C A) (@Bet Tn C A B)) *)
  destruct (col_dec A B C) as [|HNCol]; auto.
(* Goal: @Coplanar Tn M A B C *)
  exfalso.
(* Goal: False *)
  apply nnupper.
(* Goal: not upper_dim_3_axiom *)
  intro upper.
(* Goal: False *)
  apply HNCol.
(* Goal: @Col Tn A B C *)
  apply upper with P Q R; auto.
Qed.

Lemma median_planes_implies_upper_dim : median_planes_axiom -> upper_dim_3_axiom.
Proof.
(* Goal: forall _ : median_planes_axiom, upper_dim_3_axiom *)
  intros mp A B C P Q R HPQ HQR HPR; intros.
(* Goal: or (@Bet Tn A B C) (or (@Bet Tn B C A) (@Bet Tn C A B)) *)
  destruct (col_dec A B C); trivial.
(* Goal: @Coplanar Tn M A B C *)
  exfalso.
(* Goal: False *)
  apply HQR.
(* Goal: @eq (@Tpoint Tn) Q R *)
  destruct (midpoint_existence P Q) as [X].
(* Goal: @eq (@Tpoint Tn) Q R *)
  apply symmetric_point_uniqueness with P X; trivial.
(* Goal: @Midpoint Tn X P R *)
  destruct (midpoint_existence P R) as [Y].
(* Goal: @Midpoint Tn X P R *)
  replace X with Y; trivial.
(* Goal: @eq (@Tpoint Tn) Y X *)
  apply (l8_7 P); apply l8_2.
  - apply l11_60 with A B C; [|exists R; split..|]; trivial.
(* Goal: @Coplanar Tn A B C X *)
    apply mp with P Q; Cong.
  - apply l11_60 with A B C; [|exists Q; split..|]; trivial.
(* Goal: @Coplanar Tn A B C Y *)
    apply mp with P R; Cong.
Qed.

Lemma median_planes_aux :
  (forall A B C P Q M, P <> Q -> Cong A P A Q -> Cong B P B Q -> Cong C P C Q -> Midpoint M P Q ->
                       Coplanar M A B C) ->
  median_planes_axiom.
Proof.
(* Goal: forall _ : forall (A B C P Q M : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) P Q)) (_ : @Cong Tn A P A Q) (_ : @Cong Tn B P B Q) (_ : @Cong Tn C P C Q) (_ : @Midpoint Tn M P Q), @Coplanar Tn M A B C, median_planes_axiom *)
  intros Haux A B C D P Q; intros.
(* Goal: @Coplanar Tn A B C D *)
  destruct (col_dec A B C) as [HCop|]; [apply col__coplanar, HCop|].
(* Goal: @Coplanar Tn A B C D *)
  destruct (midpoint_existence P Q) as [M].
(* Goal: @Coplanar Tn A B C D *)
  destruct (ex_ncol_cop2 A B C M) as [A1 [A2 [HCop1 [HCop2 HNCol1]]]].
(* Goal: @Coplanar Tn A B C D *)
  assert (Cong A1 P A1 Q) by (apply (l11_60_aux A B C); assumption).
(* Goal: @Coplanar Tn A B C D *)
  assert (Cong A2 P A2 Q) by (apply (l11_60_aux A B C); assumption).
(* Goal: @Coplanar Tn A B C D *)
  apply coplanar_pseudo_trans with M A1 A2; eauto.
Qed.

Lemma orthonormal_family_aux : orthonormal_family_axiom <->
  (forall A B X P Q, ~ Col P Q X -> Per A X P -> Per A X Q -> Per B X P -> Per B X Q -> Col A B X).
Proof.
(* Goal: iff orthonormal_family_axiom (forall (A B X P Q : @Tpoint Tn) (_ : not (@Col Tn P Q X)) (_ : @Per Tn A X P) (_ : @Per Tn A X Q) (_ : @Per Tn B X P) (_ : @Per Tn B X Q), @Col Tn A B X) *)
  split.
  - intros up A B X P Q HNCol HAXP HAXQ HBXP HBXQ.
(* Goal: @Col Tn A B X *)
    destruct (col_dec A B X) as [|HNCol1]; [assumption|].
(* Goal: @Coplanar Tn M A B C *)
    exfalso.
(* Goal: False *)
    destruct (segment_construction P X P X) as [P' []].
(* Goal: @Col Tn A B X *)
    assert_diffs.
(* Goal: False *)
    destruct (ex_per_cong P X X Q P' X) as [Q']; Col; spliter.
(* Goal: False *)
    assert (HAXQ' : Per Q' X A) by (apply (l11_60 P Q X); Perp; Cop).
(* Goal: False *)
    assert (HBXQ' : Per Q' X B) by (apply (l11_60 P Q X); Perp; Cop).
(* Goal: False *)
    assert (HNCol' : ~ Col P X Q') by (apply one_side_not_col123 with Q; assumption).
(* Goal: @Col Tn A B X *)
    clear dependent Q.
(* Goal: False *)
    rename Q' into Q.
(* Goal: False *)
    destruct (segment_construction A X P' X) as [A' []].
(* Goal: False *)
    assert (HAXP' : Per P X A') by (assert_diffs; apply per_col with A; Perp; Col).
(* Goal: False *)
    assert (HAXQ : Per Q X A') by (assert_diffs; apply per_col with A; Perp; Col).
(* Goal: False *)
    assert (HNCol : ~ Col A' B X) by (intro; apply HNCol1; ColR).
(* Goal: False *)
    clear dependent A.
(* Goal: False *)
    rename A' into A.
(* Goal: False *)
    destruct (ex_per_cong A X X B P' X) as [B']; Col; [assert_diffs; auto|].
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Coplanar Tn A B C Q) (and (@Coplanar Tn D E F Q) (not (@eq (@Tpoint Tn) P Q)))) *)
    spliter.
(* Goal: False *)
    assert (HBXP' : Per B' X P) by (apply (l11_60 A B X); Perp; Cop).
(* Goal: False *)
    assert (HBXQ : Per B' X Q) by (apply (l11_60 A B X); Perp; Cop).
(* Goal: False *)
    clear dependent B.
(* Goal: False *)
    rename B' into B.
(* Goal: False *)
    assert (HCong : Cong Q P Q P') by (apply per_double_cong with X; [|split]; Cong).
(* Goal: @Cong Tn X P X R *)
    apply (up X P' P Q A B); repeat split; [Cong..| | | | |];
      (apply cong_transitivity with P Q; [|Cong]);
(* Goal: @Cong Tn X P X R *)
      apply l10_12 with X X; Perp; eCong.
  - intros p4col S U1' U1 U2 U3 U4 H; spliter.
(* Goal: False *)
    assert (HMid : Midpoint S U1 U1') by (split; Cong).
(* Goal: False *)
    assert (HPer21 : Per U2 S U1) by (exists U1'; split; Cong).
(* Goal: False *)
    absurd (Col U2 U1 S).
(* Goal: not (@Col Tn U2 U1 S) *)
(* Goal: @Col Tn U2 U1 S *)
      assert_diffs; apply not_col_permutation_5, per_not_col; auto.
    apply p4col with U3 U4;
      [assert_diffs; apply not_col_permutation_2, per_not_col; auto|..];
(* Goal: @Cong Tn X P X R *)
      apply (l8_10 U2 S U1); trivial; repeat split; eCong.
Qed.

Lemma upper_dim_implies_orthonormal_family_axiom : upper_dim_3_axiom -> orthonormal_family_axiom.
Proof.
(* Goal: forall (_ : orthonormal_family_axiom) (A B C P Q X : @Tpoint Tn) (_ : @Orth_at Tn X A B C X P) (_ : @Orth_at Tn X A B C X Q), @Col Tn P Q X *)
  rewrite orthonormal_family_aux.
(* Goal: forall (_ : upper_dim_3_axiom) (A B X P Q : @Tpoint Tn) (_ : not (@Col Tn P Q X)) (_ : @Per Tn A X P) (_ : @Per Tn A X Q) (_ : @Per Tn B X P) (_ : @Per Tn B X Q), @Col Tn A B X *)
  intros up A B X P Q HNCol HAXP HAXQ HBXP HBXQ.
(* Goal: @Col Tn A B X *)
  destruct (segment_construction Q X X P) as [Q' []].
(* Goal: @Col Tn A B X *)
  assert (HNCol' : ~ Col P Q' X) by (intro; apply HNCol; ColR).
(* Goal: @Col Tn A B X *)
  assert (HAXQ' : Per A X Q') by (assert_diffs; apply per_col with Q; Col).
(* Goal: @Col Tn A B X *)
  assert (HBXQ' : Per B X Q') by (assert_diffs; apply per_col with Q; Col).
(* Goal: @Col Tn A B X *)
  clear dependent Q.
(* Goal: @Col Tn A B X *)
  destruct (symmetric_point_construction P X) as [R].
(* Goal: @Col Tn A B X *)
  assert_diffs.
(* Goal: @Col Tn A B X *)
  apply up with P Q' R.
(* Goal: not (@eq (@Tpoint Tn) P R) *)
(* Goal: @Cong Tn A P A Q' *)
(* Goal: @Cong Tn B P B Q' *)
(* Goal: @Cong Tn X P X Q' *)
(* Goal: @Cong Tn A P A R *)
(* Goal: @Cong Tn B P B R *)
(* Goal: @Cong Tn X P X R *)
    auto.
(* Goal: not (@eq (@Tpoint Tn) Q' R) *)
(* Goal: not (@eq (@Tpoint Tn) P R) *)
(* Goal: @Cong Tn A P A Q' *)
(* Goal: @Cong Tn B P B Q' *)
(* Goal: @Cong Tn X P X Q' *)
(* Goal: @Cong Tn A P A R *)
(* Goal: @Cong Tn B P B R *)
(* Goal: @Cong Tn X P X R *)
    intro; subst; apply HNCol'; Col.
(* Goal: not (@eq (@Tpoint Tn) P R) *)
(* Goal: @Cong Tn A P A Q' *)
(* Goal: @Cong Tn B P B Q' *)
(* Goal: @Cong Tn X P X Q' *)
(* Goal: @Cong Tn A P A R *)
(* Goal: @Cong Tn B P B R *)
(* Goal: @Cong Tn X P X R *)
    auto.
(* Goal: @Cong Tn B P B Q' *)
(* Goal: @Cong Tn X P X Q' *)
(* Goal: @Cong Tn A P A R *)
(* Goal: @Cong Tn B P B R *)
(* Goal: @Cong Tn X P X R *)
    apply l10_12 with X X; Cong.
(* Goal: @Cong Tn B P B Q' *)
(* Goal: @Cong Tn X P X Q' *)
(* Goal: @Cong Tn A P A R *)
(* Goal: @Cong Tn B P B R *)
(* Goal: @Cong Tn X P X R *)
    apply l10_12 with X X; Cong.
(* Goal: @Cong Tn X P X R *)
    Cong.
(* Goal: @Cong Tn B P B R *)
(* Goal: @Cong Tn X P X R *)
    apply per_double_cong with X; assumption.
(* Goal: @Cong Tn B P B R *)
(* Goal: @Cong Tn X P X R *)
    apply per_double_cong with X; assumption.
(* Goal: @Cong Tn X P X R *)
    Cong.
Qed.

Lemma orthonormal_family_axiom_implies_orth_at2__col :
  orthonormal_family_axiom ->
  (forall A B C P Q X, Orth_at X A B C X P -> Orth_at X A B C X Q -> Col P Q X).
Proof.
(* Goal: forall (_ : orthonormal_family_axiom) (A B C P Q X : @Tpoint Tn) (_ : @Orth_at Tn X A B C X P) (_ : @Orth_at Tn X A B C X Q), @Col Tn P Q X *)
  rewrite orthonormal_family_aux.
(* Goal: forall (_ : forall (A B X P Q : @Tpoint Tn) (_ : not (@Col Tn P Q X)) (_ : @Per Tn A X P) (_ : @Per Tn A X Q) (_ : @Per Tn B X P) (_ : @Per Tn B X Q), @Col Tn A B X) (A B C P Q X : @Tpoint Tn) (_ : @Orth_at Tn X A B C X P) (_ : @Orth_at Tn X A B C X Q), @Col Tn P Q X *)
  intros up A B C P Q X HP HQ.
(* Goal: @Col Tn P Q X *)
  apply orth_at_chara in HP.
(* Goal: @Col Tn P Q X *)
  apply orth_at_chara in HQ.
(* Goal: @Col Tn P Q X *)
  spliter; clean.
(* Goal: @Col Tn P Q X *)
  destruct (ex_ncol_cop2 A B C X) as [D [E [HD [HE HNCol]]]].
(* Goal: not (@eq (@Tpoint Tn) P R) *)
(* Goal: @Cong Tn A P A Q' *)
(* Goal: @Cong Tn B P B Q' *)
(* Goal: @Cong Tn X P X Q' *)
(* Goal: @Cong Tn A P A R *)
(* Goal: @Cong Tn B P B R *)
(* Goal: @Cong Tn X P X R *)
  apply up with D E; [Col|apply l8_2..]; auto.
Qed.

Lemma orthonormal_family_axiom_implies_not_two_sides_one_side :
  orthonormal_family_axiom ->
  (forall A B C X Y, ~ Coplanar A B C X -> ~ Coplanar A B C Y -> ~ TSP A B C X Y -> OSP A B C X Y).
Proof.
(* Goal: forall (_ : orthonormal_family_axiom) (A B C X Y : @Tpoint Tn) (_ : not (@Coplanar Tn A B C X)) (_ : not (@Coplanar Tn A B C Y)) (_ : not (@TSP Tn A B C X Y)), @OSP Tn A B C X Y *)
  intros up A B C X Y HX HY HNTS.
(* Goal: @OSP Tn A B C X Y *)
  destruct (l11_62_existence_bis A B C X HX) as [P HOrth].
(* Goal: @OSP Tn A B C X Y *)
  assert (HOrth1 := HOrth).
(* Goal: @OSP Tn A B C X Y *)
  apply orth_at_chara in HOrth1.
(* Goal: @OSP Tn A B C X Y *)
  destruct HOrth1 as [HNCol [HPX [HP HOrth1]]].
(* Goal: @OSP Tn A B C X Y *)
  destruct (l8_21_3 A B C P Y HP HY) as [X' [T [HOrth' [HT HBet]]]].
(* Goal: @OSP Tn A B C X Y *)
  apply (col_cop_orth__orth_at _ _ _ _ _ P) in HOrth'; Col.
(* Goal: @OSP Tn A B C X Y *)
  assert (~ Coplanar A B C X') by (apply orth_at__ncop with P, HOrth').
(* Goal: @OSP Tn A B C X Y *)
  assert (HTS : TSP A B C Y X').
(* Goal: @TSP Tn A B C Y X' *)
(* Goal: @OSP Tn A B C X Y *)
    repeat split; trivial; exists T; split; assumption.
(* Goal: @OSP Tn A B C X Y *)
  exists X'; split; [|assumption].
(* Goal: @TSP Tn M A B Q P *)
  repeat split; trivial.
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Coplanar Tn A B C T) (@Bet Tn X T X')) *)
  exists P; split; [assumption|].
(* Goal: @Bet Tn X P X' *)
  apply not_out_bet.
(* Goal: @Col Tn X P X' *)
(* Goal: not (@Out Tn P X X') *)
    apply col_permutation_1, (orthonormal_family_axiom_implies_orth_at2__col up A B C); assumption.
(* Goal: not (@Out Tn P X X') *)
  intro; apply HNTS.
(* Goal: @TSP Tn A B C X Y *)
  apply l9_41_2 with X'.
(* Goal: @TSP Tn A B C X' Y *)
(* Goal: @OSP Tn A B C X' X *)
    apply l9_38, HTS.
(* Goal: @OSP Tn A B C X' X *)
  apply osp_symmetry, cop_out__osp with P; assumption.
Qed.

Lemma orthonormal_family_axiom_implies_space_separation :
  orthonormal_family_axiom -> space_separation_axiom.
Proof.
(* Goal: forall _ : orthonormal_family_axiom, space_separation_axiom *)
  intros up A B C X Y HX HY.
(* Goal: or (@TSP Tn A B C X Y) (@OSP Tn A B C X Y) *)
  destruct (tsp_dec A B C X Y).
(* Goal: or (@TSP Tn A B C X Y) (@OSP Tn A B C X Y) *)
(* Goal: or (@TSP Tn A B C X Y) (@OSP Tn A B C X Y) *)
    left; assumption.
(* Goal: or (@TSP Tn A B C X Y) (@OSP Tn A B C X Y) *)
    right; apply (orthonormal_family_axiom_implies_not_two_sides_one_side up); assumption.
Qed.

Lemma space_separation_implies_plane_intersection : space_separation_axiom -> plane_intersection_axiom.
Proof.
(* Goal: forall _ : space_separation_axiom, median_planes_axiom *)
  intro sep.
  assert (Haux : forall A B C D E P, Coplanar A B C P -> ~ Col D E P ->
    exists Q, Coplanar A B C Q /\ Coplanar D E P Q /\ P <> Q).
(* Goal: forall (X P Q M : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) P Q)) (_ : @Cong Tn A P A Q) (_ : @Cong Tn B P B Q) (_ : @Midpoint Tn M P Q) (_ : @TSP Tn M A B Q X) (_ : @Cong Tn X P X Q), False *)
(* Goal: forall (C P Q M : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) P Q)) (_ : @Cong Tn A P A Q) (_ : @Cong Tn B P B Q) (_ : @Cong Tn C P C Q) (_ : @Midpoint Tn M P Q), @Coplanar Tn M A B C *)
  { intros A B C D E P HP1 HP2.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Coplanar Tn A B C Q) (and (@Coplanar Tn D E P Q) (not (@eq (@Tpoint Tn) P Q)))) *)
    destruct (cop_dec A B C D).
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Coplanar Tn A B C Q) (and (@Coplanar Tn D E P Q) (not (@eq (@Tpoint Tn) P Q)))) *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Coplanar Tn A B C Q) (and (@Coplanar Tn D E P Q) (not (@eq (@Tpoint Tn) P Q)))) *)
      assert_diffs; exists D; repeat split; Cop.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Coplanar Tn A B C Q) (and (@Coplanar Tn D E P Q) (not (@eq (@Tpoint Tn) P Q)))) *)
    destruct (cop_dec A B C E).
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Coplanar Tn A B C Q) (and (@Coplanar Tn D E P Q) (not (@eq (@Tpoint Tn) P Q)))) *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Coplanar Tn A B C Q) (and (@Coplanar Tn D E P Q) (not (@eq (@Tpoint Tn) P Q)))) *)
      assert_diffs; exists E; repeat split; Cop.
(* Goal: not (@eq (@Tpoint Tn) P R) *)
(* Goal: @Cong Tn A P A Q' *)
(* Goal: @Cong Tn B P B Q' *)
(* Goal: @Cong Tn X P X Q' *)
(* Goal: @Cong Tn A P A R *)
(* Goal: @Cong Tn B P B R *)
(* Goal: @Cong Tn X P X R *)
    destruct (sep A B C D E); auto.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Coplanar Tn A B C Q) (and (@Coplanar Tn D E P Q) (not (@eq (@Tpoint Tn) P Q)))) *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Coplanar Tn A B C Q) (and (@Coplanar Tn D E P Q) (not (@eq (@Tpoint Tn) P Q)))) *)
      apply cop_tsp__ex_cop2; assumption.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Coplanar Tn A B C Q) (and (@Coplanar Tn D E P Q) (not (@eq (@Tpoint Tn) P Q)))) *)
      apply cop_osp__ex_cop2; assumption.
  }
(* Goal: plane_intersection_axiom *)
  intros A B C D E F P HP1 HP2.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Coplanar Tn A B C Q) (and (@Coplanar Tn D E F Q) (not (@eq (@Tpoint Tn) P Q)))) *)
  destruct (ex_ncol_cop2 D E F P) as [D' [E']].
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Coplanar Tn A B C Q) (and (@Coplanar Tn D E F Q) (not (@eq (@Tpoint Tn) P Q)))) *)
  spliter.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Coplanar Tn A B C Q) (and (@Coplanar Tn D E F Q) (not (@eq (@Tpoint Tn) P Q)))) *)
  destruct (Haux A B C D' E' P) as [Q [HQ1 [HQ2 HPQ]]]; Col.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Coplanar Tn A B C Q) (and (@Coplanar Tn D E F Q) (not (@eq (@Tpoint Tn) P Q)))) *)
  exists Q.
(* Goal: not (@eq (@Tpoint Tn) P R) *)
(* Goal: @Cong Tn A P A Q' *)
(* Goal: @Cong Tn B P B Q' *)
(* Goal: @Cong Tn X P X Q' *)
(* Goal: @Cong Tn A P A R *)
(* Goal: @Cong Tn B P B R *)
(* Goal: @Cong Tn X P X R *)
  repeat split; auto.
(* Goal: @Coplanar Tn D E F Q *)
  destruct (col_dec D E F) as [HCol|]; [apply col__coplanar, HCol|].
(* Goal: @Coplanar Tn D E F Q *)
  apply coplanar_pseudo_trans with D' E' P; Col; apply coplanar_pseudo_trans with D E F; Cop.
Qed.

Lemma plane_intersection_implies_space_separation :
  plane_intersection_axiom -> space_separation_axiom.
Proof.
(* Goal: forall _ : plane_intersection_axiom, space_separation_axiom *)
  intros pint A B C X Y HX HY.
(* Goal: or (@TSP Tn A B C X Y) (@OSP Tn A B C X Y) *)
  assert (HA : Coplanar A B C A) by Cop.
(* Goal: or (@TSP Tn A B C X Y) (@OSP Tn A B C X Y) *)
  destruct (pint A B C A X Y A HA) as [D [HD1 [HD2 HAD]]]; Cop.
(* Goal: or (@TSP Tn A B C X Y) (@OSP Tn A B C X Y) *)
  destruct (cop__one_or_two_sides A D X Y).
(* Goal: @Coplanar Tn A D X Y *)
(* Goal: not (@Col Tn X A D) *)
(* Goal: not (@Col Tn Y A D) *)
(* Goal: or (@TSP Tn A B C X Y) (@OSP Tn A B C X Y) *)
(* Goal: or (@TSP Tn A B C X Y) (@OSP Tn A B C X Y) *)
    Cop.
(* Goal: not (@Col Tn X A D) *)
(* Goal: not (@Col Tn Y A D) *)
(* Goal: or (@TSP Tn A B C X Y) (@OSP Tn A B C X Y) *)
(* Goal: or (@TSP Tn A B C X Y) (@OSP Tn A B C X Y) *)
    intro; apply HX, col_cop2__cop with A D; Col.
(* Goal: not (@Col Tn Y A D) *)
(* Goal: or (@TSP Tn A B C X Y) (@OSP Tn A B C X Y) *)
(* Goal: or (@TSP Tn A B C X Y) (@OSP Tn A B C X Y) *)
    intro; apply HY, col_cop2__cop with A D; Col.
(* Goal: or (@TSP Tn A B C X Y) (@OSP Tn A B C X Y) *)
(* Goal: or (@TSP Tn A B C X Y) (@OSP Tn A B C X Y) *)
    left; apply cop2_ts__tsp with A D; assumption.
(* Goal: or (@TSP Tn A B C X Y) (@OSP Tn A B C X Y) *)
    right; apply cop2_os__osp with A D; assumption.
Qed.

Lemma space_separation_implies_median_planes : space_separation_axiom -> median_planes_axiom.
Proof.
(* Goal: forall _ : space_separation_axiom, median_planes_axiom *)
  intro sep.
(* Goal: median_planes_axiom *)
  apply median_planes_aux.
(* Goal: forall (A B C P Q M : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) P Q)) (_ : @Cong Tn A P A Q) (_ : @Cong Tn B P B Q) (_ : @Cong Tn C P C Q) (_ : @Midpoint Tn M P Q), @Coplanar Tn M A B C *)
  intros A B.
  assert (Haux : forall X P Q M, P <> Q ->
          Cong A P A Q -> Cong B P B Q -> Midpoint M P Q -> TSP M A B Q X -> Cong X P X Q -> False).
(* Goal: forall (X P Q M : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) P Q)) (_ : @Cong Tn A P A Q) (_ : @Cong Tn B P B Q) (_ : @Midpoint Tn M P Q) (_ : @TSP Tn M A B Q X) (_ : @Cong Tn X P X Q), False *)
(* Goal: forall (C P Q M : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) P Q)) (_ : @Cong Tn A P A Q) (_ : @Cong Tn B P B Q) (_ : @Cong Tn C P C Q) (_ : @Midpoint Tn M P Q), @Coplanar Tn M A B C *)
  { intros X P Q M HPQ HA HB HM [HQ [HX [T [HT HBet]]]].
    assert (HCong : forall C, Coplanar M A B C -> Cong C P C Q).
(* Goal: forall (C : @Tpoint Tn) (_ : @Coplanar Tn M A B C), @Cong Tn C P C Q *)
(* Goal: forall _ : @Cong Tn X P X Q, False *)
      intros; apply (l11_60_aux M A B); Cong; apply ncop__ncol with Q, HQ.
(* Goal: forall _ : @Cong Tn X P X Q, False *)
    apply triangle_strict_inequality with T; Between.
(* Goal: not (@Bet Tn X T P) *)
    intro.
(* Goal: False *)
    apply (not_bet_and_out P M Q); split; [Between|].
(* Goal: @Out Tn M P Q *)
    assert (~ Coplanar M A B P) by (intro HP; apply HCong in HP; treat_equalities; auto).
(* Goal: @Out Tn M P Q *)
    assert_all_diffs_by_contradiction.
(* Goal: @Out Tn M P Q *)
    replace M with T.
(* Goal: @Out Tn T P Q *)
(* Goal: @eq (@Tpoint Tn) T M *)
      apply l6_2 with X; Between.
(* Goal: @eq (@Tpoint Tn) T M *)
    apply (col2_cop2__eq M A B P Q); Cop; ColR.
  }
(* Goal: forall (C P Q M : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) P Q)) (_ : @Cong Tn A P A Q) (_ : @Cong Tn B P B Q) (_ : @Cong Tn C P C Q) (_ : @Midpoint Tn M P Q), @Coplanar Tn M A B C *)
  intros C P Q M HPQ HA HB HC HM.
(* Goal: @Coplanar Tn M A B C *)
  destruct (cop_dec M A B C) as [HCop|HNCop]; [apply HCop|].
(* Goal: @Coplanar Tn M A B C *)
  assert (~ Col M A B) by (apply ncop__ncol with C, HNCop).
(* Goal: @Coplanar Tn M A B C *)
  assert (HQ : ~ Coplanar M A B Q).
(* Goal: not (@eq (@Tpoint Tn) P R) *)
(* Goal: @Cong Tn A P A Q' *)
(* Goal: @Cong Tn B P B Q' *)
(* Goal: @Cong Tn X P X Q' *)
(* Goal: @Cong Tn A P A R *)
(* Goal: @Cong Tn B P B R *)
(* Goal: @Cong Tn X P X R *)
    intro Ha; apply (l11_60_aux _ _ _ _ P Q) in Ha; Cong; treat_equalities; auto.
(* Goal: @Coplanar Tn M A B C *)
  exfalso.
(* Goal: False *)
  destruct (sep M A B Q C HQ HNCop).
(* Goal: not (@eq (@Tpoint Tn) P R) *)
(* Goal: @Cong Tn A P A Q' *)
(* Goal: @Cong Tn B P B Q' *)
(* Goal: @Cong Tn X P X Q' *)
(* Goal: @Cong Tn A P A R *)
(* Goal: @Cong Tn B P B R *)
(* Goal: @Cong Tn X P X R *)
    eauto.
(* Goal: False *)
  apply l7_2 in HM.
(* Goal: @Cong Tn X P X R *)
  apply (Haux C Q P M); Cong.
(* Goal: @TSP Tn M A B P C *)
  apply l9_38, l9_41_2 with Q; [|assumption].
(* Goal: @TSP Tn M A B Q P *)
  repeat split; trivial.
(* Goal: not (@eq (@Tpoint Tn) P R) *)
(* Goal: @Cong Tn A P A Q' *)
(* Goal: @Cong Tn B P B Q' *)
(* Goal: @Cong Tn X P X Q' *)
(* Goal: @Cong Tn A P A R *)
(* Goal: @Cong Tn B P B R *)
(* Goal: @Cong Tn X P X R *)
    intro Ha; apply (l11_60_aux _ _ _ _ P Q) in Ha; Cong; treat_equalities; auto.
(* Goal: @Coplanar Tn A D X Y *)
(* Goal: not (@Col Tn X A D) *)
(* Goal: not (@Col Tn Y A D) *)
(* Goal: or (@TSP Tn A B C X Y) (@OSP Tn A B C X Y) *)
(* Goal: or (@TSP Tn A B C X Y) (@OSP Tn A B C X Y) *)
  exists M; split; Between; Cop.
Qed.

Theorem upper_dim_3_equivalent_axioms : all_equiv (upper_dim_3_axiom::
                                                   orthonormal_family_axiom::
                                                   space_separation_axiom::
                                                   plane_intersection_axiom::
                                                   median_planes_axiom::
                                                   nil).
Proof.
(* Goal: all_equiv (@cons Prop upper_dim_3_axiom (@cons Prop orthonormal_family_axiom (@cons Prop space_separation_axiom (@cons Prop plane_intersection_axiom (@cons Prop median_planes_axiom (@nil Prop)))))) *)
  assert (H := upper_dim_implies_orthonormal_family_axiom).
(* Goal: all_equiv (@cons Prop upper_dim_3_axiom (@cons Prop orthonormal_family_axiom (@cons Prop space_separation_axiom (@cons Prop plane_intersection_axiom (@cons Prop median_planes_axiom (@nil Prop)))))) *)
  assert (I := orthonormal_family_axiom_implies_space_separation).
(* Goal: all_equiv (@cons Prop upper_dim_3_axiom (@cons Prop orthonormal_family_axiom (@cons Prop space_separation_axiom (@cons Prop plane_intersection_axiom (@cons Prop median_planes_axiom (@nil Prop)))))) *)
  assert (J := space_separation_implies_plane_intersection).
(* Goal: all_equiv (@cons Prop upper_dim_3_axiom (@cons Prop orthonormal_family_axiom (@cons Prop space_separation_axiom (@cons Prop plane_intersection_axiom (@cons Prop median_planes_axiom (@nil Prop)))))) *)
  assert (K := plane_intersection_implies_space_separation).
(* Goal: all_equiv (@cons Prop upper_dim_3_axiom (@cons Prop orthonormal_family_axiom (@cons Prop space_separation_axiom (@cons Prop plane_intersection_axiom (@cons Prop median_planes_axiom (@nil Prop)))))) *)
  assert (L := space_separation_implies_median_planes).
(* Goal: all_equiv (@cons Prop upper_dim_3_axiom (@cons Prop orthonormal_family_axiom (@cons Prop space_separation_axiom (@cons Prop plane_intersection_axiom (@cons Prop median_planes_axiom (@nil Prop)))))) *)
  assert (M := median_planes_implies_upper_dim).
(* Goal: not (@eq (@Tpoint Tn) P R) *)
(* Goal: @Cong Tn A P A Q' *)
(* Goal: @Cong Tn B P B Q' *)
(* Goal: @Cong Tn X P X Q' *)
(* Goal: @Cong Tn A P A R *)
(* Goal: @Cong Tn B P B R *)
(* Goal: @Cong Tn X P X R *)
  apply all_equiv__equiv; unfold all_equiv'; simpl; repeat split; tauto.
Qed.

End Upper_dim_3.