Require Import GeoCoq.Axioms.continuity_axioms.
Require Import GeoCoq.Tarski_dev.Ch07_midpoint.

Section Dedekind_archimedes.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma archimedes_aux : (forall A B C, Out A B C -> Reach A B A C) -> archimedes_axiom.
Proof.
(* Goal: forall _ : forall (A B C : @Tpoint Tn) (_ : @Out Tn A B C), @Reach Tn A B A C, @archimedes_axiom Tn *)
  intros Haux A B C D HAB.
(* Goal: @Reach Tn A B C D *)
  destruct (eq_dec_points C D).
(* Goal: @Reach Tn A B C D *)
(* Goal: @Reach Tn A B C D *)
    subst; exists B.
(* Goal: and (@Grad Tn A B B) (@Le Tn D D A B) *)
(* Goal: @Reach Tn A B C D *)
    split; Le.
(* Goal: @Grad Tn A B B *)
(* Goal: @Reach Tn A B C D *)
    apply grad_init.
(* Goal: @Reach Tn A B C D *)
  destruct (segment_construction_3 A B C D) as [E [HOut HCong]]; auto.
(* Goal: @Reach Tn A B C D *)
  destruct (Haux A B E HOut) as [B' [HGrad HLe]]; trivial.
(* Goal: @Reach Tn A B C D *)
  exists B'.
(* Goal: and (@Grad Tn A B B') (@Le Tn C D A B') *)
  split; trivial.
(* Goal: @Le Tn C D A B' *)
  apply le_transitivity with A E; Le.
Qed.

Lemma dedekind__archimedes : (forall A B C D, ~ ~ Reach A B C D -> Reach A B C D) ->
  dedekind_s_axiom -> archimedes_axiom.
Proof.
(* Goal: forall (_ : forall (A B C D : @Tpoint Tn) (_ : not (not (@Reach Tn A B C D))), @Reach Tn A B C D) (_ : @dedekind_s_axiom Tn), @archimedes_axiom Tn *)
  intros Hstab dedekind.
(* Goal: @archimedes_axiom Tn *)
  apply archimedes_aux.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Out Tn A B C), @Reach Tn A B A C *)
  intros A B C HOut.
(* Goal: @Reach Tn A B A C *)
  apply Hstab.
(* Goal: not (not (@Reach Tn A B A C)) *)
  intro HNReach.
  assert (HX : exists X, forall P Q, (Out A B P /\ ~ ~ Reach A B A P) ->
                                       (Out A B Q /\ ~ Reach A B A Q) -> Bet P X Q).
(* Goal: @Out Tn A B X1 *)
(* Goal: not (not (@Reach Tn A B A X1)) *)
  { apply dedekind.
(* Goal: @ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => forall (X Y : @Tpoint Tn) (_ : and (@Out Tn A B X) (not (not (@Reach Tn A B A X)))) (_ : and (@Out Tn A B Y) (not (@Reach Tn A B A Y))), @Bet Tn A0 X Y) *)
    exists A.
(* Goal: forall (X Y : @Tpoint Tn) (_ : and (@Out Tn A B X) (not (not (@Reach Tn A B A X)))) (_ : and (@Out Tn A B Y) (not (@Reach Tn A B A Y))), @Bet Tn A X Y *)
    intros X Y [HXOut HX] [HYOut HY].
(* Goal: @Bet Tn A X Y *)
    assert (HOut' : Out A X Y) by (apply l6_7 with B; [apply l6_6|]; trivial).
(* Goal: @Bet Tn A X Y *)
    destruct (HOut') as [_ [_ [|Habs]]]; trivial.
(* Goal: @Bet Tn A X Y *)
    exfalso.
(* Goal: False *)
    apply HX; clear HX.
(* Goal: not (@Reach Tn A B A X) *)
    intro HX.
(* Goal: False *)
    apply HY.
(* Goal: @Reach Tn A B A Y *)
    destruct HX as [B' [HGrad HLe]].
(* Goal: and (@Grad Tn A B B') (@Le Tn C D A B') *)
    exists B'; split; trivial.
(* Goal: @Le Tn A Y A B' *)
    apply le_transitivity with A X; Le.
  }
(* Goal: False *)
  destruct HX as [X HX].
(* Goal: False *)
  assert_diffs.
(* Goal: False *)
  assert (HGrad := grad_init A B).
(* Goal: False *)
  assert (HBet : Bet B X C).
(* Goal: and (@Grad Tn A B B') (@Le Tn C D A B') *)
  { apply HX; split; trivial.
(* Goal: @Out Tn A B B *)
(* Goal: not (not (@Reach Tn A B A B)) *)
(* Goal: @Out Tn A B X0 *)
      apply out_trivial; auto.
(* Goal: not (not (@Reach Tn A B A X1)) *)
    intro HAbs; apply HAbs.
(* Goal: and (@Grad Tn A B B) (@Le Tn D D A B) *)
(* Goal: @Reach Tn A B C D *)
    exists B; split; Le.
  }
(* Goal: False *)
  assert (Out A B X) by (apply out_bet_out_1 with C; auto).
(* Goal: False *)
  destruct HOut as [_ [_ [HBet2|HBet2]]]; [|exfalso; apply HNReach; exists B; split; Le].
(* Goal: False *)
  absurd (~ Reach A B A X).

  - intro HAbs.
(* Goal: False *)
    destruct (eq_dec_points X B).
(* Goal: and (@Grad Tn A B B) (@Le Tn D D A B) *)
(* Goal: @Reach Tn A B C D *)
      subst; apply HAbs; exists B; split; Le.
(* Goal: False *)
    destruct (le_cases X A A B) as [HLe|HLe].
(* Goal: and (@Grad Tn A B B) (@Le Tn D D A B) *)
(* Goal: @Reach Tn A B C D *)
      apply HAbs; exists B; split; Le.
(* Goal: False *)
    assert (Bet A B X) by (apply l6_13_1; Le).
(* Goal: False *)
    destruct HLe as [X0 [HBet1 HCong]].
(* Goal: False *)
    absurd (~ Reach A B A X0).
(* Goal: @Out Tn A B X1 *)
(* Goal: not (not (@Reach Tn A B A X1)) *)
    { intro HNReach0.
(* Goal: False *)
      assert (HXOut : Out X X0 B).
(* Goal: @Out Tn X X0 B *)
(* Goal: False *)
        apply l6_7 with A; [|apply l6_6]; apply bet_out; Between.
(* Goal: not (@eq (@Tpoint Tn) X0 X) *)
(* Goal: False *)
        intro; treat_equalities; auto.
(* Goal: False *)
      destruct (le_cases X B X X0) as [HLe|HLe].
(* Goal: and (@Grad Tn A B B') (@Le Tn C D A B') *)
      - apply HNReach0; exists B; split; trivial.
(* Goal: @Le Tn A X0 A B *)
        exists X0; split; Cong.
(* Goal: @Bet Tn A X0 B *)
        apply between_inner_transitivity with X; Between.
(* Goal: @Bet Tn X0 B X *)
        apply between_symmetry, l6_13_1; trivial.
(* Goal: @Out Tn X B X0 *)
        apply l6_6; trivial.
      - absurd (X = X0).
(* Goal: not (@eq (@Tpoint Tn) X X0) *)
(* Goal: @eq (@Tpoint Tn) X X0 *)
          assert_diffs; auto.
(* Goal: @eq (@Tpoint Tn) X X0 *)
        apply between_equality with B.
(* Goal: @Bet Tn X X0 B *)
(* Goal: @Bet Tn X0 X B *)
          apply l6_13_1; trivial.
(* Goal: and (@Grad Tn A B B') (@Le Tn C D A B') *)
        apply between_symmetry, HX; split; trivial.
(* Goal: @Out Tn A B B *)
(* Goal: not (not (@Reach Tn A B A B)) *)
(* Goal: @Out Tn A B X0 *)
          apply out_trivial; auto.
(* Goal: and (@Grad Tn A B B) (@Le Tn D D A B) *)
(* Goal: @Reach Tn A B C D *)
          intro HN; apply HN; exists B; split; Le.
(* Goal: @Out Tn A B X1 *)
        apply l6_7 with X; trivial.
(* Goal: @Out Tn A X X0 *)
        apply l6_6, bet_out; Between.
(* Goal: not (@eq (@Tpoint Tn) X0 A) *)
        intro; subst X0; apply HNReach0.
(* Goal: and (@Grad Tn A B B) (@Le Tn D D A B) *)
(* Goal: @Reach Tn A B C D *)
        exists B; split; Le.
    }
(* Goal: not (@Reach Tn A B A X) *)
    intro HReach.
(* Goal: not (not (@Reach Tn A B A X1)) *)
    destruct HReach as [B' [HGrad' HLe]].
(* Goal: not (not (@Reach Tn A B A X1)) *)
    destruct (segment_construction A B' A B) as [B1' [HBet' HCong']].
(* Goal: False *)
    apply HAbs; exists B1'; split.
(* Goal: @Grad Tn A B B1' *)
(* Goal: @Le Tn A X1 A B1' *)
      apply grad_stab with B'; Cong.
(* Goal: @Le Tn A X A B1' *)
    apply bet2_le2__le1346 with X0 B'; Le; Between.
(* Goal: @Le Tn X X1 B' B1' *)
    apply cong__le, cong_transitivity with A B; Cong.

  - intro HReach.
(* Goal: False *)
    destruct (segment_construction_3 X C A B) as [X1 [HOut' HCong]]; auto.
(* Goal: not (@eq (@Tpoint Tn) X C) *)
(* Goal: False *)
      intro; subst; contradiction.
(* Goal: False *)
    assert (HBet1 : Bet A X X1).
(* Goal: @Bet Tn A X X1 *)
(* Goal: False *)
      apply between_symmetry, bet_out__bet with C; eBetween.
(* Goal: False *)
    apply (not_bet_and_out X1 X C).
(* Goal: and (@Bet Tn X1 X C) (@Out Tn X X1 C) *)
    split; [|apply l6_6; trivial].
(* Goal: @Bet Tn X1 X C *)
    apply HX; split; trivial; [| |apply bet_out; auto].
(* Goal: @Out Tn A B X1 *)
(* Goal: not (not (@Reach Tn A B A X1)) *)
    { apply l6_7 with X; trivial.
(* Goal: @Out Tn A X X1 *)
      assert_diffs; apply bet_out; auto.
    }
(* Goal: not (not (@Reach Tn A B A X1)) *)
    destruct HReach as [B' [HGrad' HLe]].
(* Goal: not (not (@Reach Tn A B A X1)) *)
    destruct (segment_construction A B' A B) as [B1' [HBet' HCong']].
(* Goal: not (not (@Reach Tn A B A X1)) *)
    intro HAbs; apply HAbs.
(* Goal: @Reach Tn A B A X1 *)
    exists B1'; split.
(* Goal: @Grad Tn A B B1' *)
(* Goal: @Le Tn A X1 A B1' *)
      apply grad_stab with B'; Cong.
(* Goal: @Le Tn A X1 A B1' *)
    apply bet2_le2__le1346 with X B'; Le.
(* Goal: @Le Tn X X1 B' B1' *)
    apply cong__le, cong_transitivity with A B; Cong.
Qed.

End Dedekind_archimedes.