Require Import GeoCoq.Axioms.continuity_axioms.
Require Import GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2.
Require Import GeoCoq.Meta_theory.Dimension_axioms.upper_dim_3.
Require Import GeoCoq.Tarski_dev.Ch10_line_reflexivity_2.

(** This development is inspired by Theorem 32 of Hilbert's Foundations of Geometry (10th edition).
    It deduces completeness of a 2 or 3-dimensional space from completeness of lines.
    The original proof is due to Paul Bernays. *)

Section Completeness.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

(* Goal: @plane_intersection_axiom Tm *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
Lemma extension__line_extension : forall {Tm: Tarski_neutral_dimensionless}
  (f : @Tpoint Tn -> @Tpoint Tm) P Q,
  P <> Q -> extension f -> line_extension f P Q.
Proof.
(* Goal: forall (Tm : Tarski_neutral_dimensionless) (f : forall _ : @Tpoint Tn, @Tpoint Tm) (P Q : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) P Q)) (_ : @extension Tn Tm f), @line_extension Tn Tm f P Q *)
  unfold extension, inj, pres_bet, pres_cong, line_extension, inj_line, pres_bet_line, pres_cong_line.
(* Goal: forall (Tm : Tarski_neutral_dimensionless) (f : forall _ : @Tpoint Tn, @Tpoint Tm) (P Q : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) P Q)) (_ : and (forall (A B : @Tpoint Tn) (_ : @eq (@Tpoint Tm) (f A) (f B)), @eq (@Tpoint Tn) A B) (and (forall (A B C : @Tpoint Tn) (_ : @Bet Tn A B C), @Bet Tm (f A) (f B) (f C)) (forall (A B C D : @Tpoint Tn) (_ : @Cong Tn A B C D), @Cong Tm (f A) (f B) (f C) (f D)))), and (not (@eq (@Tpoint Tn) P Q)) (and (forall (A B : @Tpoint Tn) (_ : @Col Tn P Q A) (_ : @Col Tn P Q B) (_ : @eq (@Tpoint Tm) (f A) (f B)), @eq (@Tpoint Tn) A B) (and (forall (A B C : @Tpoint Tn) (_ : @Col Tn P Q A) (_ : @Col Tn P Q B) (_ : @Col Tn P Q C) (_ : @Bet Tn A B C), @Bet Tm (f A) (f B) (f C)) (forall (A B C D : @Tpoint Tn) (_ : @Col Tn P Q A) (_ : @Col Tn P Q B) (_ : @Col Tn P Q C) (_ : @Col Tn P Q D) (_ : @Cong Tn A B C D), @Cong Tm (f A) (f B) (f C) (f D)))) *)
  intros Tm f P Q HPQ fext; spliter.
(* Goal: and (not (@eq (@Tpoint Tn) P Q)) (and (forall (A B : @Tpoint Tn) (_ : @Col Tn P Q A) (_ : @Col Tn P Q B) (_ : @eq (@Tpoint Tm) (f A) (f B)), @eq (@Tpoint Tn) A B) (and (forall (A B C : @Tpoint Tn) (_ : @Col Tn P Q A) (_ : @Col Tn P Q B) (_ : @Col Tn P Q C) (_ : @Bet Tn A B C), @Bet Tm (f A) (f B) (f C)) (forall (A B C D : @Tpoint Tn) (_ : @Col Tn P Q A) (_ : @Col Tn P Q B) (_ : @Col Tn P Q C) (_ : @Col Tn P Q D) (_ : @Cong Tn A B C D), @Cong Tm (f A) (f B) (f C) (f D)))) *)
  repeat split; auto.
Qed.

(* Goal: @plane_intersection_axiom Tm *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
Lemma extension_reverse_bet : forall {Tm: Tarski_neutral_dimensionless}
(* Goal: @plane_intersection_axiom Tm *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  {Tm2 : Tarski_neutral_dimensionless_with_decidable_point_equality Tm}
  (f : @Tpoint Tn -> @Tpoint Tm),
  extension f ->
  forall A B C, Bet (f A) (f B) (f C) -> Bet A B C.
Proof.
(* Goal: forall (Tm : Tarski_neutral_dimensionless) (_ : Tarski_neutral_dimensionless_with_decidable_point_equality Tm) (f : forall _ : @Tpoint Tn, @Tpoint Tm) (_ : @extension Tn Tm f) (A B C : @Tpoint Tn) (_ : @Bet Tm (f A) (f B) (f C)), @Bet Tn A B C *)
  intros Tm Tm2 f [finj [fBet fCong]] A B C HBet.
(* Goal: @Bet Tn A B C *)
  destruct (eq_dec_points (f A) (f B)) as [Heq|].
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    apply finj in Heq; subst; Between.
(* Goal: @Bet Tn A B C *)
  destruct (segment_construction A B B C) as [D [HD1 HD2]].
(* Goal: @Bet Tn A B C *)
  assert (C = D); [|subst; auto].
(* Goal: @eq (@Tpoint Tn) C D *)
  apply finj.
(* Goal: @eq (@Tpoint Tm) (f C) (f D) *)
  apply between_cong_3 with (f A) (f B); Cong.
Qed.

(* Goal: @plane_intersection_axiom Tm *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
Lemma extension_reverse_col : forall {Tm: Tarski_neutral_dimensionless}
(* Goal: @plane_intersection_axiom Tm *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  {Tm2 : Tarski_neutral_dimensionless_with_decidable_point_equality Tm}
  (f : @Tpoint Tn -> @Tpoint Tm),
  extension f ->
  forall A B C, Col (f A) (f B) (f C) -> Col A B C.
Proof.
(* Goal: forall (Tm : Tarski_neutral_dimensionless) (_ : Tarski_neutral_dimensionless_with_decidable_point_equality Tm) (f : forall _ : @Tpoint Tn, @Tpoint Tm) (_ : @extension Tn Tm f) (A B C : @Tpoint Tn) (_ : @Col Tm (f A) (f B) (f C)), @Col Tn A B C *)
  unfold Col.
(* Goal: forall (Tm : Tarski_neutral_dimensionless) (_ : Tarski_neutral_dimensionless_with_decidable_point_equality Tm) (f : forall _ : @Tpoint Tn, @Tpoint Tm) (_ : @extension Tn Tm f) (A B C : @Tpoint Tn) (_ : or (@Bet Tm (f A) (f B) (f C)) (or (@Bet Tm (f B) (f C) (f A)) (@Bet Tm (f C) (f A) (f B)))), or (@Bet Tn A B C) (or (@Bet Tn B C A) (@Bet Tn C A B)) *)
  intros Tm Tm2 f fext A B C HCol.
(* Goal: or (@Bet Tn A B C) (or (@Bet Tn B C A) (@Bet Tn C A B)) *)
  assert (fBetInv := extension_reverse_bet f fext).
(* Goal: or (@Bet Tn A B C) (or (@Bet Tn B C A) (@Bet Tn C A B)) *)
  destruct HCol as [|[|]]; auto.
Qed.


Lemma line_completeness_aux : line_completeness ->
  forall (Tm: Tarski_neutral_dimensionless)
  (Tm2 : Tarski_neutral_dimensionless_with_decidable_point_equality Tm)
  (f : @Tpoint Tn -> @Tpoint Tm),
  @archimedes_axiom Tm ->
  extension f ->
  forall A P Q R, ~ Col P Q R -> Coplanar (f P) (f Q) (f R) A ->
    exists B, Coplanar P Q R B /\ f B = A.
Proof.
(* Goal: forall (_ : @line_completeness Tn) (Tm : Tarski_neutral_dimensionless) (_ : Tarski_neutral_dimensionless_with_decidable_point_equality Tm) (f : forall _ : @Tpoint Tn, @Tpoint Tm) (_ : @archimedes_axiom Tm) (_ : @extension Tn Tm f) (A : @Tpoint Tm) (P Q R : @Tpoint Tn) (_ : not (@Col Tn P Q R)) (_ : @Coplanar Tm (f P) (f Q) (f R) A), @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P Q R B) (@eq (@Tpoint Tm) (f B) A)) *)
  intros lc Tm Tm2 f archi fext A P Q R HNCol HCop.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P Q R B) (@eq (@Tpoint Tm) (f B) A)) *)
  assert (fext' := fext).
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P Q R B) (@eq (@Tpoint Tm) (f B) A)) *)
  assert (Haux : forall X Y, X <> Y -> line_extension f X Y).
(* Goal: forall (X Y : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) X Y)), @line_extension Tn Tm f X Y *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P Q R B) (@eq (@Tpoint Tm) (f B) A)) *)
    intros; apply extension__line_extension; assumption.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P Q R B) (@eq (@Tpoint Tm) (f B) A)) *)
  unfold extension, inj, pres_bet, pres_cong in fext'; spliter.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P Q R B) (@eq (@Tpoint Tm) (f B) A)) *)
  destruct (@midpoint_existence Tn TnEQD P Q) as [S HS].
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P Q R B) (@eq (@Tpoint Tm) (f B) A)) *)
  assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P Q R B) (@eq (@Tpoint Tm) (f B) A)) *)
  destruct (col_dec (f R) (f S) A).
(* Goal: @plane_intersection_axiom Tm *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  { assert (HB : exists B, Col R S B /\ f B = A).
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Col Tn R S B) (@eq (@Tpoint Tm) (f B) A)) *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P Q R B) (@eq (@Tpoint Tm) (f B) A)) *)
      assert (R <> S) by (intro; subst; apply HNCol; Col).
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Col Tn R S B) (@eq (@Tpoint Tm) (f B) A)) *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P Q R B) (@eq (@Tpoint Tm) (f B) A)) *)
      apply lc; auto.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
    destruct HB as [B []].
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P Q R B) (@eq (@Tpoint Tm) (f B) A)) *)
    exists B; split; [exists S; left; split|]; Col.
  }
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  destruct (col_dec (f P) (f Q) A).
(* Goal: @plane_intersection_axiom Tm *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  { assert (HB : exists B, Col P Q B /\ f B = A) by (apply lc; auto).
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
    destruct HB as [B []].
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P Q R B) (@eq (@Tpoint Tm) (f B) A)) *)
    exists B; split; Cop.
  }
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P Q R B) (@eq (@Tpoint Tm) (f B) A)) *)
  destruct (hilbert_s_version_of_pasch (f P) (f Q) (f R) A (f S)) as [X [HX1 HX2]]; trivial.
(* Goal: @BetS Tm (f P) (f S) (f Q) *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P Q R B) (@eq (@Tpoint Tm) (f B) A)) *)
    repeat split; Between.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P Q R B) (@eq (@Tpoint Tm) (f B) A)) *)
  assert (HY : exists Y, Coplanar P Q R Y /\ f Y = X).
(* Goal: @plane_intersection_axiom Tm *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  { destruct HX2 as [[]|[]];
      [assert (HY : exists Y, Col P R Y /\ f Y = X)|assert (HY : exists Y, Col Q R Y /\ f Y = X)];
      try apply lc; Col;
      destruct HY as [Y []]; exists Y; split; Cop.
  }
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P Q R B) (@eq (@Tpoint Tm) (f B) A)) *)
  destruct HY as [Y []].
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P Q R B) (@eq (@Tpoint Tm) (f B) A)) *)
  subst X.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P Q R B) (@eq (@Tpoint Tm) (f B) A)) *)
  assert (S <> Y).
(* Goal: @plane_intersection_axiom Tm *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  { intro; treat_equalities.
(* Goal: False *)
    apply HNCol.
(* Goal: @Col Tn P Q R *)
    apply (extension_reverse_col f); auto.
(* Goal: @Col Tm (f P) (f Q) (f R) *)
    assert (Bet P S Q) by Between.
(* Goal: @Col Tm (f P) (f Q) (f R) *)
    assert (Bet (f P) (f S) (f Q)) by auto.
    destruct HX2 as [[HBet []]|[HBet []]];
      [|apply col_permutation_4]; apply (col_transitivity_2 (f S)); Col.
  }
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P Q R B) (@eq (@Tpoint Tm) (f B) A)) *)
  assert (HB : exists B, Col S Y B /\ f B = A) by (apply lc; Col).
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  destruct HB as [B []].
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P Q R B) (@eq (@Tpoint Tm) (f B) A)) *)
  exists B.
(* Goal: and (@Coplanar Tn P Q R B) (@eq (@Tpoint Tm) (f B) A) *)
  split; [apply col_cop2__cop with S Y|]; Cop.
Qed.

Lemma line_completeness__completeness_for_planes : line_completeness -> completeness_for_planes.
Proof.
(* Goal: forall _ : @line_completeness Tn, @completeness_for_planes Tn *)
  intros lc Tm Tm2 M f archi fext A.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  assert (HB : exists B, Coplanar PA PB PC B /\ f B = A).
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn (@PA Tn) (@PB Tn) (@PC Tn) B) (@eq (@Tpoint Tm) (f B) A)) *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
    apply line_completeness_aux; trivial; [exact lower_dim|apply all_coplanar].
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  destruct HB as [B []].
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  exists B; assumption.
Qed.

(* Goal: @plane_intersection_axiom Tm *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
Lemma completeness_aux : forall {Tm: Tarski_neutral_dimensionless}
  P Q R (f : @Tpoint Tn -> @Tpoint Tm) A,
  (exists B, Coplanar P Q R B /\ f B = A) -> exists B, f B = A.
Proof.
(* Goal: forall (Tm : Tarski_neutral_dimensionless) (P Q R : @Tpoint Tn) (f : forall _ : @Tpoint Tn, @Tpoint Tm) (A : @Tpoint Tm) (_ : @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P Q R B) (@eq (@Tpoint Tm) (f B) A))), @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  intros Tm P Q R f A [B []].
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  exists B; assumption.
Qed.

Lemma line_completeness__completeness_for_3d_spaces :
  (exists P Q R S, ~ Coplanar P Q R S) ->
  line_completeness -> completeness_for_3d_spaces.
Proof.
(* Goal: forall (_ : @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => @ex (@Tpoint Tn) (fun S : @Tpoint Tn => not (@Coplanar Tn P Q R S)))))) (_ : @line_completeness Tn), @completeness_for_3d_spaces Tn *)
  intros [P [Q [R [S HNCop]]]] lc Tm Tm2 M f archi fext A.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  assert (~ Col P Q R) . apply ncop__ncol with S, HNCop.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  destruct (col_dec (f P) (f Q) A).
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
    apply (completeness_aux P Q R), line_completeness_aux; Cop.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  assert (pi : plane_intersection_axiom).
(* Goal: @plane_intersection_axiom Tm *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  { cut upper_dim_3_axiom.
(* Goal: forall _ : @upper_dim_3_axiom Tm, @plane_intersection_axiom Tm *)
(* Goal: @upper_dim_3_axiom Tm *)
      apply upper_dim_3_equivalent_axioms; simpl; tauto.
(* Goal: @upper_dim_3_axiom Tm *)
    unfold upper_dim_3_axiom; exact upper_dim_3.
  }
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  destruct (pi (f P) (f Q) A (f P) (f R) (f S) (f P)) as [X [HX1 [HX2 HX3]]]; Cop.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  assert (HY : exists Y, Coplanar P R S Y /\ f Y = X).
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Coplanar Tn P R S Y) (@eq (@Tpoint Tm) (f Y) X)) *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
    apply line_completeness_aux; trivial; apply ncop__ncol with Q; Cop.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  destruct HY as [Y []]; subst.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  apply completeness_aux with P Q Y, line_completeness_aux; Cop.
(* Goal: not (@Col Tn P Q Y) *)
  intro.
(* Goal: False *)
  apply HNCop.
(* Goal: @Coplanar Tn P Q R S *)
  apply coplanar_perm_16, col_cop__cop with Y; Col; Cop.
(* Goal: not (@eq (@Tpoint Tn) P Y) *)
  intro; subst; apply HX3; reflexivity.
Qed.

End Completeness.

(** In the following sections, we prove that our formalizations of Hilbert's axiom of completeness
    are always true in spaces with dimension respectively greater than 2 and 3. *)

Section Dimension.

(* Goal: @plane_intersection_axiom Tm *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
Context `{Tn:Tarski_neutral_dimensionless}.

(* Goal: @plane_intersection_axiom Tm *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
Lemma extension_to_plane__plane : forall {Tm: Tarski_neutral_dimensionless}
(* Goal: @plane_intersection_axiom Tm *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  {Tm2 : Tarski_neutral_dimensionless_with_decidable_point_equality Tm}
(* Goal: @plane_intersection_axiom Tm *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  {M : Tarski_2D Tm2}
  (f : @Tpoint Tn -> @Tpoint Tm),
  extension f ->
  @upper_dim_axiom Tn.
Proof.
(* Goal: forall (Tm : Tarski_neutral_dimensionless) (Tm2 : Tarski_neutral_dimensionless_with_decidable_point_equality Tm) (_ : @Tarski_2D Tm Tm2) (f : forall _ : @Tpoint Tn, @Tpoint Tm) (_ : @extension Tn Tm f), @upper_dim_axiom Tn *)
  intros Tm Tm2 M f fext A B C P Q HPQ H1 H2 H3.
(* Goal: or (@Bet Tn A B C) (or (@Bet Tn B C A) (@Bet Tn C A B)) *)
  apply (extension_reverse_col f); trivial.
(* Goal: @Col Tm (f A) (f B) (f C) *)
  unfold extension, inj, pres_cong in fext; spliter.
(* Goal: @Col Tm (f A) (f B) (f C) *)
  unfold Col; apply upper_dim with (f P) (f Q); auto.
Qed.

Lemma nupper_dim__completeness_for_planes : ~ upper_dim_axiom -> completeness_for_planes.
Proof.
(* Goal: forall _ : not (@upper_dim_3_axiom Tn), @completeness_for_3d_spaces Tn *)
  intros lowerdim Tm Tm2 M f archi fext A.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  exfalso; apply lowerdim.
(* Goal: @upper_dim_axiom Tn *)
  apply extension_to_plane__plane with f; trivial.
Qed.

(* Goal: @plane_intersection_axiom Tm *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
Lemma extension_to_3d__upper_dim_3 : forall {Tm: Tarski_neutral_dimensionless}
(* Goal: @plane_intersection_axiom Tm *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  {Tm2 : Tarski_neutral_dimensionless_with_decidable_point_equality Tm}
(* Goal: @plane_intersection_axiom Tm *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  {M : Tarski_3D Tm2}
  (f : @Tpoint Tn -> @Tpoint Tm),
  extension f ->
  @upper_dim_3_axiom Tn.
Proof.
(* Goal: forall (Tm : Tarski_neutral_dimensionless) (Tm2 : Tarski_neutral_dimensionless_with_decidable_point_equality Tm) (_ : @Tarski_3D Tm Tm2) (f : forall _ : @Tpoint Tn, @Tpoint Tm) (_ : @extension Tn Tm f), @upper_dim_3_axiom Tn *)
  intros Tm Tm2 M f fext 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)) *)
  apply (extension_reverse_col f); trivial.
(* Goal: @Col Tm (f A) (f B) (f C) *)
  unfold extension, inj, pres_cong in fext; spliter.
(* Goal: @Col Tm (f A) (f B) (f C) *)
  unfold Col; apply upper_dim_3 with (f P) (f Q) (f R); auto.
Qed.

Lemma nupper_dim_3__completeness_for_3d_spaces : ~ upper_dim_3_axiom -> completeness_for_3d_spaces.
Proof.
(* Goal: forall _ : not (@upper_dim_3_axiom Tn), @completeness_for_3d_spaces Tn *)
  intros lowerdim Tm Tm2 M f archi fext A.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @eq (@Tpoint Tm) (f B) A) *)
  exfalso; apply lowerdim.
(* Goal: @upper_dim_3_axiom Tn *)
  apply extension_to_3d__upper_dim_3 with f; trivial.
Qed.

End Dimension.


Section Dimension'.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma ncompleteness_for_planes__upper_dim : ~ completeness_for_planes -> upper_dim_axiom.
Proof.
(* Goal: forall _ : not (@completeness_for_3d_spaces Tn), @upper_dim_3_axiom Tn *)
  intro nc.
(* Goal: @upper_dim_axiom Tn *)
  apply upper_dim_stab.
(* Goal: not (not (@upper_dim_3_axiom Tn)) *)
  intro nupper.
(* Goal: False *)
  apply nc, (nupper_dim__completeness_for_planes nupper).
Qed.

Lemma ncompleteness_for_3d_spaces__upper_dim_3 : ~ completeness_for_3d_spaces -> upper_dim_3_axiom.
Proof.
(* Goal: forall _ : not (@completeness_for_3d_spaces Tn), @upper_dim_3_axiom Tn *)
  intro nc.
(* Goal: @upper_dim_3_axiom Tn *)
  apply upper_dim_3_stab.
(* Goal: not (not (@upper_dim_3_axiom Tn)) *)
  intro nupper.
(* Goal: False *)
  apply nc, (nupper_dim_3__completeness_for_3d_spaces nupper).
Qed.

End Dimension'.