Require Import GeoCoq.Axioms.continuity_axioms.
Require Import GeoCoq.Meta_theory.Continuity.completeness.
Require Import GeoCoq.Meta_theory.Continuity.grad.
Require Import GeoCoq.Tarski_dev.Ch08_orthogonality.

(** This file contains the proof that Dedekind completeness implies Hilbert's line completeness. *)

Section Line_extension.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
Lemma line_extension_symmetry : forall {Tm : Tarski_neutral_dimensionless}
  (f : @Tpoint Tn -> @Tpoint Tm) P Q, line_extension f P Q -> line_extension f Q P.
Proof.
(* Goal: forall (Tm : Tarski_neutral_dimensionless) (f : forall _ : @Tpoint Tn, @Tpoint Tm) (P Q : @Tpoint Tn) (_ : @line_extension Tn Tm f P Q), @line_extension Tn Tm f Q P *)
  intros Tm f P Q [HPQ [fInj [fBet fCong]]].
(* Goal: @line_extension Tn Tm f Q P *)
  repeat split; auto; intro; intros; [apply fInj|apply fBet|apply fCong]; Col.
Qed.

(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
Lemma line_extension_stability : forall {Tm: Tarski_neutral_dimensionless}
  (f : @Tpoint Tn -> @Tpoint Tm) P Q R,
  Col P Q R -> P <> R -> line_extension f P Q -> line_extension f P R.
Proof.
(* Goal: forall (Tm : Tarski_neutral_dimensionless) (f : forall _ : @Tpoint Tn, @Tpoint Tm) (P Q R : @Tpoint Tn) (_ : @Col Tn P Q R) (_ : not (@eq (@Tpoint Tn) P R)) (_ : @line_extension Tn Tm f P Q), @line_extension Tn Tm f P R *)
  intros Tm f P Q R HCol HPR [HPQ [fInj [fBet fCong]]].
  repeat split; auto; intro; intros;
    [apply fInj|apply fBet|apply fCong]; trivial; apply col_transitivity_1 with R; Col.
Qed.

(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
Lemma line_extension_reverse_bet : forall {Tm: Tarski_neutral_dimensionless}
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
  {Tm2: Tarski_neutral_dimensionless_with_decidable_point_equality Tm}
  (f : @Tpoint Tn -> @Tpoint Tm) P Q, line_extension f P Q ->
  forall A B C, Col P Q A -> Col P Q B -> Col P Q 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) (P Q : @Tpoint Tn) (_ : @line_extension Tn Tm f P Q) (A B C : @Tpoint Tn) (_ : @Col Tn P Q A) (_ : @Col Tn P Q B) (_ : @Col Tn P Q C) (_ : @Bet Tm (f A) (f B) (f C)), @Bet Tn A B C *)
  intros Tm Tm2 f P Q [HPQ [fInj [fBet fCong]]] A B C HA HB HC HBet.
(* Goal: @Bet Tn A B C *)
  destruct (eq_dec_points (f A) (f B)) as [Heq|Hdiff].
(* Goal: @Bet Tn A B C *)
(* Goal: @Bet Tn A B C *)
    apply fInj in Heq; subst; Between.
(* Goal: @Bet Tn A B C *)
  assert (A <> B) by (intro; subst; auto).
(* 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 *)
  assert (Col P Q D) by (apply (colx A B); Col).
(* Goal: @eq (@Tpoint Tn) C D *)
  apply fInj; trivial.
(* Goal: @eq (@Tpoint Tm) (f C) (f D) *)
  apply between_cong_3 with (f A) (f B); Cong.
Qed.

(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
Lemma pres_bet_line__col : forall {Tm: Tarski_neutral_dimensionless}
  f (P Q : @Tpoint Tn), P <> Q -> pres_bet_line f P Q ->
  forall A B C, Col P Q A -> Col P Q B -> Col P Q C -> Col (f A) (f B) (f C).
Proof.
(* Goal: forall (Tm : Tarski_neutral_dimensionless) (f : forall _ : @Tpoint Tn, @Tpoint Tm) (P Q : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) P Q)) (_ : @pres_bet_line Tn Tm f P Q) (A B C : @Tpoint Tn) (_ : @Col Tn P Q A) (_ : @Col Tn P Q B) (_ : @Col Tn P Q C), @Col Tm (f A) (f B) (f C) *)
  intros Tm f P Q HPQ fBet A B C HA HB HC.
(* Goal: @Col Tm (f A) (f B) (f C) *)
  destruct (col3 P Q A B C) as [HBet|[HBet|HBet]]; trivial; apply fBet in HBet; Col.
Qed.

End Line_extension.

Section Completeness.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

(** If there exists n such that (f A) X = n times (f A) (f B),
    then X belongs to the image of the line extension f *)

(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
Lemma extension_grad : forall {Tm: Tarski_neutral_dimensionless}
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
  {Tm2 : Tarski_neutral_dimensionless_with_decidable_point_equality Tm}
  P Q (f : @Tpoint Tn -> @Tpoint Tm),
  line_extension f P Q ->
  forall A B X, Col P Q A -> Col P Q B -> Grad (f A) (f B) X ->
  exists C, Col P Q C /\ Grad A B C /\ f C = X.
Proof.
(* Goal: forall (Tm : Tarski_neutral_dimensionless) (_ : Tarski_neutral_dimensionless_with_decidable_point_equality Tm) (P Q : @Tpoint Tn) (f : forall _ : @Tpoint Tn, @Tpoint Tm) (_ : @line_extension Tn Tm f P Q) (A B : @Tpoint Tn) (X : @Tpoint Tm) (_ : @Col Tn P Q A) (_ : @Col Tn P Q B) (_ : @Grad Tm (f A) (f B) X), @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@Grad Tn A B C) (@eq (@Tpoint Tm) (f C) X))) *)
  intros Tm Tm2 P Q f [HPQ [fInj [fBet fCong]]] A B X HA HB HGrad.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@Grad Tn A B C) (@eq (@Tpoint Tm) (f C) X))) *)
  destruct (eq_dec_points A B).
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
  { subst B.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@Grad Tn A A C) (@eq (@Tpoint Tm) (f C) X))) *)
    apply grad112__eq in HGrad; subst X.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@Grad Tn A A C) (@eq (@Tpoint Tm) (f C) (f A)))) *)
    exists A; repeat split; [assumption|constructor].
  }
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@Grad Tn A B C) (@eq (@Tpoint Tm) (f C) X))) *)
  remember (f A) as A0.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@Grad Tn A B C) (@eq (@Tpoint Tm) (f C) X))) *)
  remember (f B) as B0.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@Grad Tn A B C) (@eq (@Tpoint Tm) (f C) X))) *)
  induction HGrad.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@GradExp Tn A C B) (@eq (@Tpoint Tm) (f C) B0))) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@GradExp Tn A C B) (@eq (@Tpoint Tm) (f C) B'))) *)
    exists B; repeat split; auto; constructor.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@Grad Tn A B C) (@eq (@Tpoint Tm) (f C) C'))) *)
  rename C into X, C' into X'.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@Grad Tn A B C) (@eq (@Tpoint Tm) (f C) X'))) *)
  destruct IHHGrad as [C [HC1 [HC2 HC3]]]; trivial.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@Grad Tn A B C) (@eq (@Tpoint Tm) (f C) X'))) *)
  assert (A0 <> X).
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
  { intro; subst X.
(* Goal: False *)
    assert (A = C) by (apply fInj; auto; congruence).
(* Goal: False *)
    subst.
(* Goal: False *)
    apply grad121__eq in HGrad.
(* Goal: False *)
    apply fInj in HGrad; auto.
  }
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@Grad Tn A B C) (@eq (@Tpoint Tm) (f C) X'))) *)
  destruct (segment_construction A C A B) as [C' [HC'1 HC'2]].
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@Grad Tn A B C) (@eq (@Tpoint Tm) (f C) X'))) *)
  exists C'.
(* Goal: and (@Col Tn P Q C') (and (@Grad Tn A B C') (@eq (@Tpoint Tm) (f C') X')) *)
  assert (Col P Q C').
(* Goal: @Col Tn P Q C' *)
(* Goal: and (@Col Tn P Q C') (and (@Grad Tn A B C') (@eq (@Tpoint Tm) (f C') X')) *)
    apply (colx A C); Col; apply grad_neq__neq13 with B; auto.
(* Goal: and (@Col Tn P Q C') (and (@Grad Tn A B C') (@eq (@Tpoint Tm) (f C') X')) *)
  repeat split; trivial.
(* Goal: @Grad Tn A B C' *)
(* Goal: @eq (@Tpoint Tm) (f C') X' *)
    apply grad_stab with C; Cong.
(* Goal: @eq (@Tpoint Tm) (f C') X' *)
  apply (construction_uniqueness A0 X A0 B0); Cong; subst; auto.
Qed.

(** If there exists n such that (f A) X = (f A) (f B) divided by 2^n,
    then X belongs to the image of the line extension f *)

(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
Lemma extension_gradexp : forall {Tm: Tarski_neutral_dimensionless}
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
  {Tm2 : Tarski_neutral_dimensionless_with_decidable_point_equality Tm}
  P Q (f : @Tpoint Tn -> @Tpoint Tm),
  line_extension f P Q ->
  forall A B X, Col P Q A -> Col P Q B -> GradExp (f A) X (f B) ->
  exists C, Col P Q C /\ GradExp A C B /\ f C = X.
Proof.
(* Goal: forall (Tm : Tarski_neutral_dimensionless) (_ : Tarski_neutral_dimensionless_with_decidable_point_equality Tm) (P Q : @Tpoint Tn) (f : forall _ : @Tpoint Tn, @Tpoint Tm) (_ : @line_extension Tn Tm f P Q) (A B : @Tpoint Tn) (X : @Tpoint Tm) (_ : @Col Tn P Q A) (_ : @Col Tn P Q B) (_ : @GradExp Tm (f A) X (f B)), @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@GradExp Tn A C B) (@eq (@Tpoint Tm) (f C) X))) *)
  intros Tm Tm2 P Q f [HPQ [fInj [fBet fCong]]] A B X HA HB.
(* Goal: forall _ : @GradExp Tm (f A) X (f B), @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@GradExp Tn A C B) (@eq (@Tpoint Tm) (f C) X))) *)
  remember (f A) as A'.
(* Goal: forall _ : @GradExp Tm A' X (f B), @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@GradExp Tn A C B) (@eq (@Tpoint Tm) (f C) X))) *)
  remember (f B) as B'.
(* Goal: @GradExp Tn A M B *)
(* Goal: @eq (@Tpoint Tm) (f M) B' *)
  rewrite gradexp__gradexpinv.
(* Goal: forall _ : @GradExpInv Tm A' X B', @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@GradExp Tn A C B) (@eq (@Tpoint Tm) (f C) X))) *)
  induction 1.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@GradExp Tn A C B) (@eq (@Tpoint Tm) (f C) B0))) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@GradExp Tn A C B) (@eq (@Tpoint Tm) (f C) B'))) *)
    exists B; repeat split; auto; constructor.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@GradExp Tn A C B) (@eq (@Tpoint Tm) (f C) B'))) *)
  destruct IHGradExpInv as [C' [HCol []]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@GradExp Tn A C B) (@eq (@Tpoint Tm) (f C) B'))) *)
  destruct (midpoint_existence A C') as [M []].
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Col Tn P Q C) (and (@GradExp Tn A C B) (@eq (@Tpoint Tm) (f C) B'))) *)
  assert (Col P Q M).
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
  { destruct (eq_dec_points A C').
(* Goal: @Col Tn P Q M *)
(* Goal: @Col Tn P Q M *)
      treat_equalities; assumption.
(* Goal: @Col Tn P Q M *)
    apply colx with A C'; Col.
  }
(* Goal: and (@Col Tn P Q C') (and (@Grad Tn A B C') (@eq (@Tpoint Tm) (f C') X')) *)
  exists M; repeat split; trivial.
(* Goal: @GradExp Tn A M B *)
(* Goal: @eq (@Tpoint Tm) (f M) B' *)
    rewrite gradexp__gradexpinv.
(* Goal: @GradExpInv Tn A M B *)
(* Goal: @eq (@Tpoint Tm) (f M) B' *)
    apply gradexpinv_stab with C'; trivial.
(* Goal: @GradExpInv Tn A C' B *)
(* Goal: @eq (@Tpoint Tm) (f M) B' *)
    rewrite <- gradexp__gradexpinv; assumption.
(* Goal: @eq (@Tpoint Tm) (f M) B' *)
  apply l7_17 with A0 B0; split; trivial; subst; [apply fBet|apply fCong]; assumption.
Qed.

(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
Lemma extension_image_density_aux : forall {Tm: Tarski_neutral_dimensionless}
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
  {Tm2 : Tarski_neutral_dimensionless_with_decidable_point_equality Tm}
  P Q (f : @Tpoint Tn -> @Tpoint Tm),
  @archimedes_axiom Tm ->
  line_extension f P Q ->
  forall A B, A <> B ->
  Lt (f P) (f Q) A B -> Bet (f P) (f Q) A -> Bet (f P) A B ->
  exists X, Col P Q X /\ Bet A (f X) B /\ f X <> A /\ f X <> B.
Proof.
(* Goal: forall (Tm : Tarski_neutral_dimensionless) (_ : Tarski_neutral_dimensionless_with_decidable_point_equality Tm) (P Q : @Tpoint Tn) (f : forall _ : @Tpoint Tn, @Tpoint Tm) (_ : @archimedes_axiom Tm) (_ : @line_extension Tn Tm f P Q) (A B : @Tpoint Tm) (_ : not (@eq (@Tpoint Tm) A B)) (_ : @Lt Tm (f P) (f Q) A B) (_ : @Bet Tm (f P) (f Q) A) (_ : @Bet Tm (f P) A B), @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
  intros Tm Tm2 P Q f archi fLineExt A B HAB HLt HBet1 HBet2.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
  cut (exists C, Grad (f P) (f Q) C /\ Bet A C B /\ C <> A /\ C <> B).
(* Goal: forall _ : @ex (@Tpoint Tm) (fun C : @Tpoint Tm => and (@Grad Tm (f P) (f Q) C) (and (@Bet Tm A C B) (and (not (@eq (@Tpoint Tm) C A)) (not (@eq (@Tpoint Tm) C B))))), @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
(* Goal: @ex (@Tpoint Tm) (fun C : @Tpoint Tm => and (@Grad Tm (f P) (f Q) C) (and (@Bet Tm A C B) (and (not (@eq (@Tpoint Tm) C A)) (not (@eq (@Tpoint Tm) C B))))) *)
    intros [C [HC1 [HC2 [HC3 HC4]]]].
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
(* Goal: @ex (@Tpoint Tm) (fun C : @Tpoint Tm => and (@Grad Tm (f P) (f Q) C) (and (@Bet Tm A C B) (and (not (@eq (@Tpoint Tm) C A)) (not (@eq (@Tpoint Tm) C B))))) *)
    destruct (extension_grad P Q f fLineExt P Q C) as [X]; Col.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
(* Goal: @ex (@Tpoint Tm) (fun C : @Tpoint Tm => and (@Grad Tm (f P) (f Q) C) (and (@Bet Tm A C B) (and (not (@eq (@Tpoint Tm) C A)) (not (@eq (@Tpoint Tm) C B))))) *)
    exists X; spliter; subst; auto.
(* Goal: @ex (@Tpoint Tm) (fun C : @Tpoint Tm => and (@Grad Tm (f P) (f Q) C) (and (@Bet Tm A C B) (and (not (@eq (@Tpoint Tm) C A)) (not (@eq (@Tpoint Tm) C B))))) *)
  assert (Hdiff : f P <> f Q).
(* Goal: not (@eq (@Tpoint Tm) (f P) (f Q)) *)
(* Goal: @ex (@Tpoint Tm) (fun C : @Tpoint Tm => and (@Grad Tm (f P) (f Q) C) (and (@Bet Tm A C B) (and (not (@eq (@Tpoint Tm) C A)) (not (@eq (@Tpoint Tm) C B))))) *)
    intro; destruct fLineExt as [HPQ [fInj]]; apply HPQ, fInj; Col.
(* Goal: @ex (@Tpoint Tm) (fun C : @Tpoint Tm => and (@Grad Tm (f P) (f Q) C) (and (@Bet Tm A C B) (and (not (@eq (@Tpoint Tm) C A)) (not (@eq (@Tpoint Tm) C B))))) *)
  destruct (reach__grad_min (f P) (f Q) A) as [D [E [HD1 [HD2 [HE1 [HE2 [HDE1 HDE2]]]]]]]; auto.
(* Goal: @ex (@Tpoint Tm) (fun C : @Tpoint Tm => and (@Grad Tm (f P) (f Q) C) (and (@Bet Tm A C B) (and (not (@eq (@Tpoint Tm) C A)) (not (@eq (@Tpoint Tm) C B))))) *)
  assert (Bet D A E) by (apply (between_exchange3 (f P)); assumption).
(* Goal: @ex (@Tpoint Tm) (fun C : @Tpoint Tm => and (@Grad Tm (f P) (f Q) C) (and (@Bet Tm A C B) (and (not (@eq (@Tpoint Tm) C A)) (not (@eq (@Tpoint Tm) C B))))) *)
  assert (Le A E D E) by Le.
(* Goal: @ex (@Tpoint Tm) (fun C : @Tpoint Tm => and (@Grad Tm (f P) (f Q) C) (and (@Bet Tm A C B) (and (not (@eq (@Tpoint Tm) C A)) (not (@eq (@Tpoint Tm) C B))))) *)
  exists E; repeat split; auto.
  - apply grad_stab with D; assumption.
  - apply l6_13_1.
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
    { destruct (eq_dec_points A D).
(* Goal: @Out Tm A E B *)
(* Goal: @Out Tm A E B *)
        subst D; apply l6_2 with (f P); Between; apply bet_neq12__neq with (f Q); assumption.
(* Goal: @Out Tm A E B *)
      apply l6_2 with D; Between.
(* Goal: @Bet Tm B A D *)
        apply between_symmetry, (between_exchange3 (f P)); assumption.
    }
(* Goal: @Le Tm A E A B *)
    apply le_transitivity with D E; trivial.
(* Goal: @Le Tm (f P) (f Q') (f P) B *)
    apply le_transitivity with (f P) (f Q); Le.
  - intro; subst E.
(* Goal: False *)
    apply lt__nle in HLt.
(* Goal: False *)
    apply HLt, le_transitivity with D B; Le.
Qed.

(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
Lemma extension_image_density_aux2 : forall {Tm: Tarski_neutral_dimensionless}
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
  {Tm2 : Tarski_neutral_dimensionless_with_decidable_point_equality Tm}
  P Q (f : @Tpoint Tn -> @Tpoint Tm),
  @archimedes_axiom Tm ->
  line_extension f P Q ->
  forall A B, A <> B -> Col (f P) (f Q) A -> Col (f P) (f Q) B ->
  Lt (f P) (f Q) A B -> Bet (f P) A B ->
  exists X, Col P Q X /\ Bet A (f X) B /\ f X <> A /\ f X <> B.
Proof.
(* Goal: forall (Tm : Tarski_neutral_dimensionless) (_ : Tarski_neutral_dimensionless_with_decidable_point_equality Tm) (P Q : @Tpoint Tn) (f : forall _ : @Tpoint Tn, @Tpoint Tm) (_ : @archimedes_axiom Tm) (_ : @line_extension Tn Tm f P Q) (A B : @Tpoint Tm) (_ : not (@eq (@Tpoint Tm) A B)) (_ : @Col Tm (f P) (f Q) A) (_ : @Col Tm (f P) (f Q) B) (_ : @Lt Tm (f P) (f Q) A B) (_ : @Bet Tm (f P) A B), @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
  assert (Haux := line_extension_symmetry).
(* Goal: forall (Tm : Tarski_neutral_dimensionless) (_ : Tarski_neutral_dimensionless_with_decidable_point_equality Tm) (P Q : @Tpoint Tn) (f : forall _ : @Tpoint Tn, @Tpoint Tm) (_ : @archimedes_axiom Tm) (_ : @line_extension Tn Tm f P Q) (A B : @Tpoint Tm) (_ : not (@eq (@Tpoint Tm) A B)) (_ : @Col Tm (f P) (f Q) A) (_ : @Col Tm (f P) (f Q) B) (_ : @Lt Tm (f P) (f Q) A B) (_ : @Bet Tm (f P) A B), @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
  intros Tm Tm2 P Q f archi fLineExt A B HAB HColA HColB HLt HBet.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
  assert (Hf' := fLineExt); destruct Hf' as [HPQ [fInj [fBet fCong]]].
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A)) *)
  destruct (eq_dec_points (f P) A).
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
  { treat_equalities.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm (f P) (f X) B) (and (not (@eq (@Tpoint Tm) (f X) (f P))) (not (@eq (@Tpoint Tm) (f X) B))))) *)
    assert (f P <> f Q) by (intro; apply HPQ, fInj; Col).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm (f P) (f X) B) (and (not (@eq (@Tpoint Tm) (f X) (f P))) (not (@eq (@Tpoint Tm) (f X) B))))) *)
    destruct (or_bet_out (f Q) (f P) B) as [HBet|[HOut|]]; [..|exfalso; Col].
    - destruct (segment_construction Q P P Q) as [Q' []].
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm (f Q) (f X) B) (and (not (@eq (@Tpoint Tm) (f X) (f Q))) (not (@eq (@Tpoint Tm) (f X) B))))) *)
      exists Q'.
(* Goal: and (@Col Tn P Q Q') (and (@Bet Tm (f P) (f Q') B) (and (not (@eq (@Tpoint Tm) (f Q') (f P))) (not (@eq (@Tpoint Tm) (f Q') B)))) *)
      assert (HBet' : Bet (f Q) (f P) (f Q')) by (apply fBet; Col).
(* Goal: and (@Col Tn P Q Q') (and (@Bet Tm (f P) (f Q') B) (and (not (@eq (@Tpoint Tm) (f Q') (f P))) (not (@eq (@Tpoint Tm) (f Q') B)))) *)
      assert (HCong' : Cong (f P) (f Q') (f P) (f Q)) by (apply fCong; Col).
(* Goal: and (@Col Tn P Q Q') (and (@Bet Tm (f P) (f Q') B) (and (not (@eq (@Tpoint Tm) (f Q') (f P))) (not (@eq (@Tpoint Tm) (f Q') B)))) *)
      assert (f P <> f Q').
(* Goal: not (@eq (@Tpoint Tm) (f P) (f Q')) *)
(* Goal: and (@Col Tn P Q Q') (and (@Bet Tm (f P) (f Q') B) (and (not (@eq (@Tpoint Tm) (f Q') (f P))) (not (@eq (@Tpoint Tm) (f Q') B)))) *)
        intro; assert (P = Q') by (apply fInj; Col); assert_diffs; auto.
(* Goal: and (@Col Tn P Q Q) (and (@Bet Tm A (f Q) B) (and (not (@eq (@Tpoint Tm) (f Q) A)) (not (@eq (@Tpoint Tm) (f Q) B)))) *)
      repeat split; Col.
(* Goal: @Bet Tm (f P) (f Q') B *)
      * apply l6_13_1.
(* Goal: @Out Tm (f P) (f Q') B *)
(* Goal: @Le Tm (f P) (f Q') (f P) B *)
          apply l6_2 with (f Q); Between.
(* Goal: @Le Tm (f P) (f Q') (f P) B *)
          apply le_transitivity with (f P) (f Q); Le.
      * intro; subst; destruct HLt; Cong.
    - exists Q; repeat split; Col.
(* Goal: @Bet Tm (f P) (f Q) B *)
(* Goal: not (@eq (@Tpoint Tm) (f Q) B) *)
        apply l6_13_1; Le.
(* Goal: not (@eq (@Tpoint Tm) (f Q) B) *)
        intro; subst; destruct HLt; Cong.
  }
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
  destruct HColA as [|[|]].
  - apply (extension_image_density_aux P Q); trivial.
  - destruct (eq_dec_points (f Q) A).
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
    { treat_equalities.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm (f Q) (f X) B) (and (not (@eq (@Tpoint Tm) (f X) (f Q))) (not (@eq (@Tpoint Tm) (f X) B))))) *)
      destruct (segment_construction P Q P Q) as [Q' []].
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm (f Q) (f X) B) (and (not (@eq (@Tpoint Tm) (f X) (f Q))) (not (@eq (@Tpoint Tm) (f X) B))))) *)
      exists Q'.
(* Goal: and (@Col Tn P Q Q') (and (@Bet Tm (f Q) (f Q') B) (and (not (@eq (@Tpoint Tm) (f Q') (f Q))) (not (@eq (@Tpoint Tm) (f Q') B)))) *)
      assert (HBet' : Bet (f P) (f Q) (f Q')) by (apply fBet; Col).
(* Goal: and (@Col Tn P Q Q') (and (@Bet Tm (f Q) (f Q') B) (and (not (@eq (@Tpoint Tm) (f Q') (f Q))) (not (@eq (@Tpoint Tm) (f Q') B)))) *)
      assert (HCong' : Cong (f Q) (f Q') (f P) (f Q)) by (apply fCong; Col).
(* Goal: and (@Col Tn P Q Q') (and (@Bet Tm (f Q) (f Q') B) (and (not (@eq (@Tpoint Tm) (f Q') (f Q))) (not (@eq (@Tpoint Tm) (f Q') B)))) *)
      assert (f Q <> f Q') by (assert_diffs; auto).
(* Goal: and (@Col Tn P Q Q') (and (@Bet Tm (f Q) (f Q') B) (and (not (@eq (@Tpoint Tm) (f Q') (f Q))) (not (@eq (@Tpoint Tm) (f Q') B)))) *)
      assert (HLt2 : Lt (f Q) (f Q') (f Q) B) by (apply (cong2_lt__lt (f P) (f Q) (f Q) B); Cong).
(* Goal: and (@Col Tn P Q Q) (and (@Bet Tm A (f Q) B) (and (not (@eq (@Tpoint Tm) (f Q) A)) (not (@eq (@Tpoint Tm) (f Q) B)))) *)
      repeat split; Col.
(* Goal: @Bet Tm A (f Q) B *)
(* Goal: not (@eq (@Tpoint Tm) (f Q) B) *)
        apply l6_13_1; Le; apply l6_2 with (f P); Between.
(* Goal: not (@eq (@Tpoint Tm) (f Q) B) *)
        intro; subst; destruct HLt2; Cong.
    }
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
    exists Q.
(* Goal: and (@Col Tn P Q Q) (and (@Bet Tm A (f Q) B) (and (not (@eq (@Tpoint Tm) (f Q) A)) (not (@eq (@Tpoint Tm) (f Q) B)))) *)
    assert (HLt2 : Lt A (f Q) A B) by (apply le1234_lt__lt with (f P) (f Q); Le).
(* Goal: and (@Col Tn P Q Q) (and (@Bet Tm A (f Q) B) (and (not (@eq (@Tpoint Tm) (f Q) A)) (not (@eq (@Tpoint Tm) (f Q) B)))) *)
    repeat split; Col.
(* Goal: @Bet Tm A (f Q) B *)
(* Goal: not (@eq (@Tpoint Tm) (f Q) B) *)
      apply l6_13_1; Le; apply l6_2 with (f P); Between.
(* Goal: not (@eq (@Tpoint Tm) (f Q) B) *)
      intro; subst; destruct HLt2; Cong.
  - apply line_extension_symmetry in fLineExt.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
    destruct (extension_image_density_aux Q P f archi fLineExt A B) as [X]; Between.
(* Goal: @Lt Tm (f Q) (f P) A B *)
(* Goal: @Bet Tm (f Q) A B *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
      apply lt_left_comm, HLt.
(* Goal: @Bet Tm (f Q) A B *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
      apply outer_transitivity_between2 with (f P); Between.
(* Goal: and (@Col Tn P Q Q) (and (@Bet Tm A (f Q) B) (and (not (@eq (@Tpoint Tm) (f Q) A)) (not (@eq (@Tpoint Tm) (f Q) B)))) *)
    spliter; exists X; repeat split; Col.
Qed.

(** Given a line extension f to a line l in an Archimedean space, the image of f is dense in l *)

(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
Lemma extension_image_density : forall {Tm: Tarski_neutral_dimensionless}
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
  {Tm2 : Tarski_neutral_dimensionless_with_decidable_point_equality Tm}
  P Q (f : @Tpoint Tn -> @Tpoint Tm),
  @archimedes_axiom Tm ->
  line_extension f P Q ->
  forall A B, Col (f P) (f Q) A -> Col (f P) (f Q) B -> A <> B ->
  exists X, Col P Q X /\ Bet A (f X) B /\ f X <> A /\ f X <> B.
Proof.
(* Goal: forall (Tm : Tarski_neutral_dimensionless) (_ : Tarski_neutral_dimensionless_with_decidable_point_equality Tm) (P Q : @Tpoint Tn) (f : forall _ : @Tpoint Tn, @Tpoint Tm) (_ : @archimedes_axiom Tm) (_ : @line_extension Tn Tm f P Q) (A B : @Tpoint Tm) (_ : @Col Tm (f P) (f Q) A) (_ : @Col Tm (f P) (f Q) B) (_ : not (@eq (@Tpoint Tm) A B)), @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
  intros Tm Tm2 P Q f archi fLineExt A B HA HB HAB.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
  assert (Hf' := fLineExt); destruct Hf' as [HPQ [fInj [fBet fCong]]].
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
  assert (f P <> f Q).
(* Goal: not (@eq (@Tpoint Tm) (f P) (f Q)) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
    intro; apply HPQ, fInj; Col.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
  destruct (reach__ex_gradexp_lt (f P) (f Q) A B) as [fQ' [HGrad' HLt]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
  destruct (extension_gradexp P Q f fLineExt P Q fQ') as [Q' [HCol [HGrad]]]; Col.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
  subst fQ'.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
  apply gradexp__grad in HGrad; apply gradexp__grad in HGrad'.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
  assert (HPQ' : P <> Q').
(* Goal: not (@eq (@Tpoint Tn) P Q') *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
    intro; subst; apply grad112__eq in HGrad; auto.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
  assert (fLineExt' : line_extension f P Q').
(* Goal: @line_extension Tn Tm f P Q' *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
    apply line_extension_stability with Q; auto.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
  assert (HCols : Col (f P) (f Q') A /\ Col (f P) (f Q') B /\ Col (f P) A B).
(* Goal: and (@Col Tm (f P) (f Q') A) (and (@Col Tm (f P) (f Q') B) (@Col Tm (f P) A B)) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
    split; [|split]; apply col_transitivity_1 with (f Q); Col.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
  destruct HCols as [HA' [HB' Hdij]].
  assert (HColX : forall X, Col P Q' X -> Col P Q X).
(* Goal: forall (X : @Tpoint Tn) (_ : @Col Tn P Q' X), @Col Tn P Q X *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
    intros; apply col_transitivity_1 with Q'; Col.
  assert (HH : Bet (f P) A B -> exists X, Col P Q X /\ Bet A (f X) B /\ f X <> A /\ f X <> B).
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
  { intro HBet.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
    destruct (extension_image_density_aux2 P Q' f archi fLineExt' A B) as [X]; auto.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
    exists X; spliter; repeat split; auto.
  }
  assert (HH' : Bet (f P) B A -> exists X, Col P Q X /\ Bet A (f X) B /\ f X <> A /\ f X <> B).
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
  { intro HBet.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
    destruct (extension_image_density_aux2 P Q' f archi fLineExt' B A) as [X [HX1 [HX2 []]]]; auto.
(* Goal: @Lt Tm (f P) (f Q') B A *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
      apply lt_right_comm, HLt.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
    exists X; repeat split; Between.
  }
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
  destruct Hdij as [|[|]].
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
    apply HH; trivial.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
    apply HH'; Between.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A)) *)
  destruct (eq_dec_points (f P) A).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
    subst; apply HH; Between.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
  destruct (eq_dec_points (f P) B).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
    subst; apply HH'; Between.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (and (@Bet Tm A (f X) B) (and (not (@eq (@Tpoint Tm) (f X) A)) (not (@eq (@Tpoint Tm) (f X) B))))) *)
  exists P; repeat split; finish.
Qed.

Lemma dedekind__completeness : dedekind_s_axiom -> line_completeness.
Proof.
(* Goal: forall _ : @dedekind_s_axiom Tn, @line_completeness Tn *)
  intros dedekind Tm Tm2 P Q f archi fLineExt A HA.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A)) *)
  destruct (eq_dec_points (f P) A).
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A)) *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A)) *)
    subst; exists P; split; Col.
  destruct (dedekind (fun X => Col P Q X /\ Bet (f P) (f X) A)
    (fun X => Col P Q X /\ Bet (f P) A (f X))) as [B HB].
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
  { exists P.
(* Goal: forall (X Y : @Tpoint Tn) (_ : and (@Col Tn P Q X) (@Bet Tm (f P) (f X) A)) (_ : and (@Col Tn P Q Y) (@Bet Tm (f P) A (f Y))), @Bet Tn P X Y *)
    intros X Y [] [].
(* Goal: @Bet Tn P X Y *)
    apply (line_extension_reverse_bet f P Q); Col.
(* Goal: @Bet Tm (f P) (f X) (f Y) *)
    eBetween.
  }
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A)) *)
  exists B.
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
  assert (HR : exists R, Col P Q R /\ Bet (f P) A (f R)).
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
  { destruct (segment_construction (f P) A (f P) A) as [A' []].
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
    assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
    destruct (extension_image_density P Q f archi fLineExt A A') as [R [HR1 [HR2 []]]]; Col.
(* Goal: @Col Tm (f P) (f Q) A' *)
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Col Tn P Q R) (@Bet Tm (f P) A (f R))) *)
      apply col_transitivity_1 with A; Col.
(* Goal: @Bet Tm (f P) (f X) (f Y) *)
    exists R; split; eBetween.
  }
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
  destruct HR as [R []].
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
  assert (HBet : Bet P B R).
(* Goal: @Bet Tm (f P) (f X) (f Y) *)
    apply HB; split; finish; eBetween.
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
  assert (Col P Q B).
(* Goal: @Col Tn P Q B *)
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
    apply col_transitivity_1 with R; Col; intro; treat_equalities; auto.
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
  destruct (eq_dec_points (f B) A); [split; assumption|].
(* Goal: and (@Col Tn P Q B) (@eq (@Tpoint Tm) (f B) A) *)
  exfalso.
(* Goal: False *)
  assert (Hf := fLineExt).
(* Goal: False *)
  destruct Hf as [HPQ [finj [fBet fCong]]].
(* Goal: False *)
  destruct (extension_image_density P Q f archi fLineExt A (f B)) as [X [HX1 [HX2 [HX3 Habs]]]]; auto.
(* Goal: @Col Tm (f P) (f Q) (f B) *)
(* Goal: False *)
    apply (pres_bet_line__col f P Q); Col.
(* Goal: False *)
  destruct (l5_3 (f P) A (f B) (f R)); auto; [apply fBet; Col|apply Habs..].
  - apply between_equality with (f P).
(* Goal: @Bet Tm (f X) (f B) (f P) *)
(* Goal: @Bet Tm (f B) (f X) (f P) *)
      apply between_symmetry, fBet, HB; try split; Col; Between.
(* Goal: @Bet Tm (f P) A (f X) *)
(* Goal: @Bet Tm (f B) (f X) (f P) *)
      apply between_inner_transitivity with (f B); assumption.
(* Goal: @Bet Tm (f P) (f X) (f Y) *)
    clear dependent R; eBetween.
  - apply between_equality with (f P).
(* Goal: @Bet Tm (f P) (f X) (f Y) *)
      clear dependent R; eBetween.
(* Goal: @Bet Tm (f B) (f X) (f P) *)
    apply between_exchange3 with (f R).
(* Goal: @Bet Tm (f P) (f X) (f Y) *)
      apply between_symmetry, fBet; Col; apply HB; split; Col; eBetween.
(* Goal: @Bet Tm (f R) (f X) (f P) *)
    apply bet3__bet with A (f B); finish.
Qed.

End Completeness.