Require Import GeoCoq.Axioms.continuity_axioms.
Require Import GeoCoq.Tarski_dev.Annexes.saccheri.
Require Import GeoCoq.Tarski_dev.Ch13_1.
Require Import GeoCoq.Meta_theory.Continuity.grad.

(** This development is inspired by The Foundations of Geometry and the Non-Euclidean Plane, by George E Martin, chapter 22 *)

Section Archimedes.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.


(** For every m, there exists n such that A0Dm = A0An - E0En = n(A0A1 - E0E1) (m=n) *)
Lemma t22_18_aux1 : forall A0 A1 E0 E1 D1 D,
  Bet A0 D1 A1 -> Cong E0 E1 A1 D1 ->
  Grad A0 D1 D ->
  exists A E, Grad2 A0 A1 A E0 E1 E /\ Cong E0 E A D /\ Bet A0 D A.
Proof.
(* Goal: forall (A0 A1 E0 E1 D1 D : @Tpoint Tn) (_ : @Bet Tn A0 D1 A1) (_ : @Cong Tn E0 E1 A1 D1) (_ : @Grad Tn A0 D1 D), @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Grad2 Tn A0 A1 A E0 E1 E) (and (@Cong Tn E0 E A D) (@Bet Tn A0 D A)))) *)
  intros A0 A1 E0 E1 D1 D HBet HCong HG.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Grad2 Tn A0 A1 A E0 E1 E) (and (@Cong Tn E0 E A D) (@Bet Tn A0 D A)))) *)
  induction HG.
(* Goal: @ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Grad2 Tn A A1 A0 E0 E1 E) (and (@Cong Tn E0 E A0 B) (@Bet Tn A B A0)))) *)
(* Goal: @ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Grad2 Tn A A1 A0 E0 E1 E) (and (@Cong Tn E0 E A0 C') (@Bet Tn A C' A0)))) *)
    exists A1; exists E1; repeat split; auto; apply grad2_init.
(* Goal: @ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Grad2 Tn A A1 A0 E0 E1 E) (and (@Cong Tn E0 E A0 C') (@Bet Tn A C' A0)))) *)
  rename A into A0.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Grad2 Tn A0 A1 A E0 E1 E) (and (@Cong Tn E0 E A C') (@Bet Tn A0 C' A)))) *)
  rename B into C1.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Grad2 Tn A0 A1 A E0 E1 E) (and (@Cong Tn E0 E A C') (@Bet Tn A0 C' A)))) *)
  destruct IHHG as [A [E [HG2 [HCong2 HBet2]]]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Grad2 Tn A0 A1 A E0 E1 E) (and (@Cong Tn E0 E A C') (@Bet Tn A0 C' A)))) *)
  destruct (segment_construction A0 A A0 A1) as [A' [HBet3 HCong3]].
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Grad2 Tn A0 A1 A E0 E1 E) (and (@Cong Tn E0 E A C') (@Bet Tn A0 C' A)))) *)
  destruct (segment_construction E0 E E0 E1) as [E' [HBet4 HCong4]].
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Grad2 Tn A0 A1 A E0 E1 E) (and (@Cong Tn E0 E A C') (@Bet Tn A0 C' A)))) *)
  exists A'; exists E'.
(* Goal: and (@Grad2 Tn A0 A1 A' E0 E1 E') (and (@Cong Tn E0 E' A' C') (@Bet Tn A0 C' A')) *)
  assert(HBet5 : Bet A0 C' A').
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
  { assert(HBet5 : Bet A0 C A') by eBetween.
(* Goal: @Bet Tn A0 C' A' *)
    assert(Bet C C' A'); [|eBetween].
(* Goal: @Bet Tn C C' A' *)
    apply grad2__grad123 in HG2.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @Saccheri Tn A0 B0 B A) *)
    apply grad__bet in HG.
(* Goal: @Bet Tn C C' A' *)
    apply grad__bet in HG2.
(* Goal: @Bet Tn C C' A' *)
    elim(eq_dec_points A0 C).
(* Goal: forall _ : @eq (@Tpoint Tn) C C', @Bet Tn C C' A' *)
(* Goal: forall _ : not (@eq (@Tpoint Tn) C C'), @Bet Tn C C' A' *)
      intro; treat_equalities; Between.
(* Goal: forall _ : not (@eq (@Tpoint Tn) A' C), @Bet Tn C C' A' *)
    intro.
(* Goal: @Bet Tn C C' A' *)
    elim(eq_dec_points C C').
(* Goal: forall _ : @eq (@Tpoint Tn) C C', @Bet Tn C C' A' *)
(* Goal: forall _ : not (@eq (@Tpoint Tn) C C'), @Bet Tn C C' A' *)
      intro; treat_equalities; Between.
(* Goal: forall _ : not (@eq (@Tpoint Tn) A' C), @Bet Tn C C' A' *)
    intro.
(* Goal: @Bet Tn C C' A' *)
    elim(eq_dec_points A' C).
(* Goal: forall _ : @eq (@Tpoint Tn) A' C, @Bet Tn C C' A' *)
(* Goal: forall _ : not (@eq (@Tpoint Tn) A' C), @Bet Tn C C' A' *)
      intro; subst A'; assert (A=C) by (apply (between_equality _ _ A0); Between); treat_equalities; Between.
(* Goal: forall _ : not (@eq (@Tpoint Tn) A' C), @Bet Tn C C' A' *)
    intro.
(* Goal: @Bet Tn C C' A' *)
    apply l6_13_1.
(* Goal: @Out Tn C C' A' *)
(* Goal: @Le Tn C C' C A' *)
      destruct (l6_2 C' A' A0 C); Between.
(* Goal: @Le Tn C C' C A' *)
    apply (le_transitivity _ _ A A').
(* Goal: @Le Tn C C' A A' *)
(* Goal: @Le Tn A A' C A' *)
      apply (l5_6 A0 C1 A0 A1); Cong; exists C1; split; Cong.
(* Goal: @Le Tn A A' C A' *)
    destruct(l5_12_a C A A'); eBetween.
  }
(* Goal: and (@Grad2 Tn A0 A1 A' E0 E1 E') (and (@Cong Tn E0 E' A' C') (@Bet Tn A0 C' A')) *)
  repeat split; auto.
(* Goal: @Grad2 Tn A0 A1 A' E0 E1 E' *)
(* Goal: @Cong Tn E0 E' A' C' *)
    apply grad2_stab with A E; Cong.
(* Goal: @Cong Tn E0 E' A' C' *)
  assert (HD : Le E0 E1 A A').
(* Goal: @Le Tn E0 E1 A A' *)
(* Goal: @Cong Tn E0 E' A' C' *)
    apply (l5_6 E0 E1 A1 A0); Cong; exists C1; split; Between.
(* Goal: @Cong Tn E0 E' A' C' *)
  destruct HD as [D [HBet6 HCong6]].
(* Goal: @Cong Tn E0 E' A' C' *)
  apply (cong_transitivity _ _ C D).
(* Goal: @Cong Tn E0 E' C D *)
(* Goal: @Cong Tn C D A' C' *)
    apply (l2_11 _ E _ _ A); Cong; eBetween; apply cong_transitivity with E0 E1; trivial.
(* Goal: @Cong Tn C D A' C' *)
  assert (Bet C D A') by eBetween.
(* Goal: @Cong Tn C D A' C' *)
  apply (l4_3 _ _ A' _ _ C); Cong; eBetween.
(* Goal: @Cong Tn D A' C' C *)
  apply (cong_transitivity _ _ A0 C1); Cong.
(* Goal: @Cong Tn D A' A0 C1 *)
  apply cong_left_commutativity; apply (l4_3 _ _ A _ _ A1); Between; Cong.
(* Goal: @Cong Tn D A C1 A1 *)
  apply cong_transitivity with E0 E1; Cong.
Qed.

(** For every n, B0Bn is lower than or equal to n times B0B1 *)
Lemma t22_18_aux2 : forall A0 A1 B0 B1 A B E,
  Saccheri A0 B0 B1 A1 ->
  Grad2 A0 A1 A B0 B1 E -> Saccheri A0 B0 B A -> Le B0 B B0 E.
Proof.
(* Goal: forall (A0 A1 B0 B1 A B E : @Tpoint Tn) (_ : @Saccheri Tn A0 B0 B1 A1) (_ : @Grad2 Tn A0 A1 A B0 B1 E) (_ : @Saccheri Tn A0 B0 B A), @Le Tn B0 B B0 E *)
  intros A0 A1 B0 B1 A B E HSac1 HG.
(* Goal: forall _ : @Saccheri Tn A0 B0 B A, @Le Tn B0 B B0 E *)
  revert B.
(* Goal: forall (B : @Tpoint Tn) (_ : @Saccheri Tn A0 B0 B A), @Le Tn B0 B B0 E *)
  induction HG; rename A into A0; rename B into A1; rename D into B0; rename E into B1.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
  { intros B HSac.
(* Goal: @Le Tn B0 B B0 B1 *)
    assert(B = B1); [|subst B; Le].
(* Goal: @eq (@Tpoint Tn) B B1 *)
    assert(Hdiff := sac_distincts A0 B0 B1 A1 HSac1); unfold Saccheri in *; spliter.
(* Goal: @eq (@Tpoint Tn) B B1 *)
    apply (l6_11_uniqueness A1 A0 B0 B1); Cong; [|apply out_trivial; auto].
(* Goal: @Out Tn A1 B B1 *)
    apply (col_one_side_out _ A0).
(* Goal: @Col Tn A1 B B1 *)
(* Goal: @OS Tn A1 A0 B B1 *)
      apply col_permutation_2, cop_per2__col with A0; Perp.
(* Goal: @Coplanar Tn A0 B B1 A1 *)
(* Goal: @OS Tn A1 A0 B B1 *)
      apply coplanar_perm_3, coplanar_trans_1 with B0; Cop.
(* Goal: not (@Col Tn B0 A0 A1) *)
(* Goal: @OS Tn A1 A0 B B1 *)
      apply not_col_permutation_2, one_side_not_col123 with B1; assumption.
(* Goal: @OS Tn A1 A0 B B1 *)
    apply (one_side_transitivity _ _ _ B0); Side.
  }
(* Goal: forall (B : @Tpoint Tn) (_ : @Saccheri Tn A0 B0 B C'), @Le Tn B0 B B0 F' *)
  rename C into A; rename F into E; rename C' into A'; rename F' into E'.
(* Goal: forall (B : @Tpoint Tn) (_ : @Saccheri Tn A0 B0 B A'), @Le Tn B0 B B0 E' *)
  intros B' HSac'.
(* Goal: @Le Tn B0 B' B0 E' *)
  assert (A0 <> A).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
  { intro; treat_equalities.
(* Goal: False *)
    assert (A0 = A1) by (apply between_identity, grad__bet, (grad2__grad123 _ _ _ B0 B1 E); auto).
(* Goal: False *)
    treat_equalities.
(* Goal: False *)
    apply sac_distincts in HSac1; spliter; auto.
  }
(* Goal: @Le Tn B0 B' B0 E' *)
  assert (HB : exists B, Saccheri A0 B0 B A).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
  { clear dependent A'; clear dependent B'; clear IHHG.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @Saccheri Tn A0 B0 B A) *)
    apply grad2__grad123 in HG.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @Saccheri Tn A0 B0 B A) *)
    apply grad__bet in HG.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @Saccheri Tn A0 B0 B A) *)
    destruct (l10_15 A0 A1 A B0) as [P [HPerp HOS]]; Col.
(* Goal: not (@Col Tn A0 A1 B0) *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @Saccheri Tn A0 B0 B A) *)
      assert (HH := sac__ncol124 A0 B0 B1 A1); Col.
(* Goal: @Lt Tn A0 D A0 C *)
    destruct (l6_11_existence A A0 B0 P) as [B [HOut Hcong5]].
(* Goal: not (@eq (@Tpoint Tn) P A) *)
(* Goal: not (@eq (@Tpoint Tn) A0 B0) *)
(* Goal: @Lt Tn A0 D A0 C *)
      assert_diffs; auto.
(* Goal: not (@eq (@Tpoint Tn) A0 B0) *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @Saccheri Tn A0 B0 B A) *)
      assert(Hdiff := sac_distincts A0 B0 B1 A1 HSac1); spliter; auto.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @Saccheri Tn A0 B0 B A) *)
    exists B.
(* Goal: @Saccheri Tn A0 B0 B A *)
    unfold Saccheri in *; spliter; assert_diffs.
(* Goal: and (@Bet Tn A N C) (and (@Lambert Tn N L B C) (@Cong Tn B L A N)) *)
    repeat split; Cong.
    - apply (per_col _ _ A1); Col.
    - apply perp_per_2; auto.
(* Goal: @Perp Tn A A0 A B *)
      apply (perp_col1 _ _ _ P); Col.
(* Goal: @Perp Tn A A0 A P *)
      apply perp_comm; apply (perp_col _ A1); Col.
    - apply invert_one_side.
(* Goal: @OS Tn A A0 B0 B *)
      apply (out_out_one_side _ _ _ P); [|apply l6_6; auto].
(* Goal: @OS Tn A A0 B0 P *)
      apply invert_one_side.
(* Goal: @OS Tn A0 A B0 P *)
      apply (col_one_side _ A1); Col.
  }
(* Goal: @Le Tn B0 B' B0 E' *)
  destruct HB as [B HSac].
(* Goal: @Le Tn B0 B' B0 E' *)
  assert (HLe := HSac).
(* Goal: @Le Tn B0 B' B0 E' *)
  apply IHHG in HLe; auto.
(* Goal: @Le Tn B0 B' B0 E' *)
  clear IHHG.
(* Goal: @Le Tn B0 B' B0 E' *)
  destruct (segment_construction B0 B E E') as [C [HBet HCong]].
(* Goal: @Le Tn B0 B' B0 E' *)
  assert (Cong B0 B1 B B').
(* Goal: @Cong Tn B0 B1 B B' *)
(* Goal: @Le Tn B0 B' B0 E' *)
    apply (cong2_sac2__cong A0 B0 B1 A1 A _ _ A'); auto; [|unfold Saccheri in *; spliter; Cong].
(* Goal: @Saccheri Tn A B B' A' *)
(* Goal: @Le Tn B0 B' B0 E' *)
    apply cop_sac2__sac with A0 B0; Cop.
(* Goal: False *)
    intro; treat_equalities; apply sac_distincts in HSac1; spliter; auto.
(* Goal: @Le Tn B0 B' B0 E' *)
  apply (le_transitivity _ _ B0 C).
(* Goal: @Le Tn B0 B' B0 C *)
(* Goal: @Le Tn B0 C B0 E' *)
    apply (triangle_inequality B0 B B' C); trivial.
(* Goal: @Cong Tn B B' B C *)
(* Goal: @Le Tn B0 C B0 E' *)
    apply cong_transitivity with E E'; Cong.
(* Goal: @Cong Tn B B' E E' *)
(* Goal: @Le Tn B0 C B0 E' *)
    apply cong_transitivity with B0 B1; Cong.
(* Goal: @Le Tn B0 C B0 E' *)
  apply (bet2_le2__le1346 _ B _ _ E); Le.
Qed.

Lemma t22_18 :
  archimedes_axiom ->
  forall A0 B0 B1 A1, Saccheri A0 B0 B1 A1 -> ~ Lt B0 B1 A1 A0.
Proof.
(* Goal: forall (_ : @archimedes_axiom Tn) (A0 B0 B1 A1 : @Tpoint Tn) (_ : @Saccheri Tn A0 B0 B1 A1), not (@Lt Tn B0 B1 A1 A0) *)
  intros Harchi A0 B0 B1 A1 HSac.
(* Goal: not (@Lt Tn B0 B1 A1 A0) *)
  intro Hlt.
(* Goal: False *)
  destruct Hlt as [Hle HNcong].
(* Goal: False *)
  destruct Hle as [D1 [Hbet Hcong]].
(* Goal: False *)
  destruct (segment_construction A0 D1 A0 B0) as [C0 [Hbet2 Hcong2]].
(* Goal: False *)
  destruct (segment_construction A0 C0 A0 B0) as [C [Hbet3 Hcong3]].
  assert(H : forall D, Grad A0 D1 D -> Lt A0 D A0 C).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
  { intros D HG.
(* Goal: @Lt Tn A0 D A0 C *)
    destruct (t22_18_aux1 A0 A1 B0 B1 D1 D) as [A [E [HG2 [Hcong4 Hbet4]]]]; Between.
(* Goal: @Lt Tn A0 D A0 C *)
    assert (Hbet5 := grad2__grad123 A0 A1 A B0 B1 E HG2).
(* Goal: @Lt Tn A0 D A0 C *)
    apply grad__bet in Hbet5.
(* Goal: @Lt Tn A0 D A0 C *)
    destruct (l10_15 A0 A1 A B0) as [P [HPerp HOS]].
(* Goal: @Col Tn A0 A1 A *)
(* Goal: not (@Col Tn A0 A1 B0) *)
(* Goal: @Lt Tn A0 D A0 C *)
      Col.
(* Goal: @Col Tn A0 A1 A *)
(* Goal: not (@Col Tn A0 A1 B0) *)
(* Goal: @Lt Tn A0 D A0 C *)
      assert (H := sac__ncol124 A0 B0 B1 A1); Col.
(* Goal: @Lt Tn A0 D A0 C *)
    destruct (l6_11_existence A A0 B0 P) as [B [HOut Hcong5]].
(* Goal: not (@eq (@Tpoint Tn) P A) *)
(* Goal: not (@eq (@Tpoint Tn) A0 B0) *)
(* Goal: @Lt Tn A0 D A0 C *)
      assert_diffs; auto.
(* Goal: not (@eq (@Tpoint Tn) A0 B0) *)
(* Goal: @Lt Tn A0 D A0 C *)
      assert(Hdiff := sac_distincts A0 B0 B1 A1 HSac); spliter; auto.
(* Goal: @Lt Tn A0 D A0 C *)
    assert(HSac2 : Saccheri A0 B0 B A).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
    { unfold Saccheri in *; spliter; assert_diffs; assert(A0 <> A) by (intro; treat_equalities; auto).
(* Goal: and (@Bet Tn A N C) (and (@Lambert Tn N L B C) (@Cong Tn B L A N)) *)
      repeat split; Cong.
      - apply (per_col _ _ A1); Col.
      - apply perp_per_2; auto.
(* Goal: @Perp Tn A A0 A B *)
        apply (perp_col1 _ _ _ P); Col.
(* Goal: @Perp Tn A A0 A P *)
        apply perp_comm; apply (perp_col _ A1); Col.
      - apply invert_one_side.
(* Goal: @OS Tn A A0 B0 B *)
        apply (out_out_one_side _ _ _ P); [|apply l6_6; auto].
(* Goal: @OS Tn A A0 B0 P *)
        apply invert_one_side.
(* Goal: @OS Tn A0 A B0 P *)
        apply (col_one_side _ A1); Col.
    }
(* Goal: @Lt Tn A0 D A0 C *)
    assert(HLe : Le B0 B B0 E) by (apply (t22_18_aux2 A0 A1 B0 B1 A); auto).
(* Goal: @Lt Tn A0 D A0 C *)
    assert (HLe2 : Le B0 B A A0).
(* Goal: @Le Tn B0 B A A0 *)
(* Goal: @Lt Tn A0 D A0 C *)
      apply (le_transitivity _ _ B0 E); auto.
(* Goal: @Le Tn B0 E A A0 *)
(* Goal: @Lt Tn A0 D A0 C *)
      apply (l5_6 A D A A0); Cong.
(* Goal: @Le Tn A D A A0 *)
(* Goal: @Lt Tn A0 D A0 C *)
      destruct (l5_12_a A D A0); Between.
(* Goal: @Lt Tn A0 D A0 C *)
    assert (HLe2' := HLe2).
(* Goal: @Lt Tn A0 D A0 C *)
    destruct HLe2' as [Q [Hbet6 Hcong6]].
(* Goal: @Lt Tn A0 D A0 C *)
    apply (le1234_lt__lt _ _ A0 Q).
(* Goal: @Le Tn A0 D A0 Q *)
(* Goal: @Lt Tn A0 Q A0 C *)
      apply (bet2_le2__le1245 _ _ A _ _ A); Between; Le.
(* Goal: @Le Tn Q A D A *)
(* Goal: @Lt Tn A0 Q A0 C *)
      apply (l5_6 B0 B B0 E); Cong.
(* Goal: @Lt Tn A0 Q A0 C *)
    clear dependent D; clear dependent E.
    destruct (l6_11_existence A0 A0 B0 A) as [B0' [HOut2 Hcong4]];
      try (assert_diffs; intro; treat_equalities; auto).
(* Goal: @Lt Tn A0 Q A0 C *)
    destruct (segment_construction A0 B0' B0 B) as [B' [Hbet7 Hcong7]].
(* Goal: @Lt Tn A0 Q A0 C *)
    destruct (segment_construction B0' B' B A) as [A' [Hbet8 Hcong8]].
(* Goal: @Lt Tn A0 Q A0 C *)
    assert (Le A0 A A0 A'). (** A0A' = A0B0 + B0B + BA *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
    { destruct (segment_construction A0 B0' B0 A) as [B'' [Hbet9 Hcong9]].
(* Goal: @Le Tn A0 A A0 A' *)
      apply (le_transitivity _ _ A0 B'').
(* Goal: @Le Tn A0 A A0 B'' *)
(* Goal: @Le Tn A0 B'' A0 A' *)
        apply (triangle_inequality_2 _ B0 _ _ B0'); Cong.
(* Goal: @Le Tn A0 B'' A0 A' *)
      apply (bet2_le2__le1346 _ B0' _ _ B0'); Le.
(* Goal: @Bet Tn A0 B0' A' *)
(* Goal: @Le Tn B0' B'' B0' A' *)
        apply (outer_transitivity_between _ _ B'); auto.
(* Goal: not (@eq (@Tpoint Tn) B0' B') *)
(* Goal: @Le Tn B0' B'' B0' A' *)
        intro; treat_equalities; apply sac_distincts in HSac2; spliter; auto.
(* Goal: @Le Tn B0' B'' B0' A' *)
      apply (l5_6 B0 A B0' A'); Cong.
(* Goal: @Le Tn B0 A B0' A' *)
      apply (triangle_inequality_2 _ B _ _ B'); Cong.
    }
(* Goal: @Lt Tn A0 Q A0 C *)
    assert (HLe3 : Le B0 B A' B0').
(* Goal: @Le Tn B0 B A' B0' *)
(* Goal: @Lt Tn A0 Q A0 C *)
      apply (l5_6 B0' B' B0' A'); Cong; destruct (l5_12_a B0' B' A'); auto.
(* Goal: @Lt Tn A0 Q A0 C *)
    destruct HLe3 as [Q' [Hbet9 Hcong9]].
(* Goal: @Lt Tn A0 Q A0 C *)
    assert (HBet10 : Bet A0 B0' A').
(* Goal: @Cong Tn B0' Q' A' B' *)
      apply sac_distincts in HSac2; spliter; assert_diffs.
(* Goal: @Bet Tn A0 B0' A' *)
(* Goal: @Lt Tn A0 Q A0 C *)
      apply (outer_transitivity_between _ _ B'); Between.
(* Goal: @Lt Tn A0 Q A0 C *)
    apply (le1234_lt__lt _ _ A0 Q').
(* Goal: @Le Tn A0 Q A0 Q' *)
(* Goal: @Lt Tn A0 Q' A0 C *)
      apply (bet2_le2__le1245 _ _ A' _ _ A); eBetween.
(* Goal: @Le Tn Q' A' Q A *)
(* Goal: @Lt Tn A0 Q' A0 C *)
      apply cong__le; apply (cong_transitivity _ _ B0 B); Cong.
(* Goal: @Lt Tn A0 Q' A0 C *)
    assert (Cong B0' Q' A0 B0).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
    { apply (cong_transitivity _ _ A B); Cong.
(* Goal: @Cong Tn B0' Q' A B *)
      apply (cong_transitivity _ _ A' B'); Cong.
(* Goal: @Cong Tn B0' Q' A' B' *)
      assert(Hcong10 : Cong B0' B' A' Q') by (apply (cong_transitivity _ _ B0 B); auto).
(* Goal: @Cong Tn B0' Q' A' B' *)
      elim(bet_dec B0' Q' B').
(* Goal: forall _ : @Bet Tn B0' Q' B', @Cong Tn B0' Q' A' B' *)
(* Goal: forall _ : not (@Bet Tn B0' Q' B'), @Cong Tn B0' Q' A' B' *)
        intro; apply (l4_3 _ _ B' _ _ Q'); Cong; eBetween.
(* Goal: forall _ : not (@Bet Tn B0' Q' B'), @Cong Tn B0' Q' A' B' *)
      intro HNBet.
(* Goal: @Cong Tn B0' Q' A' B' *)
      apply sac_distincts in HSac2; spliter; assert_diffs.
(* Goal: @Cong Tn B0' Q' A' B' *)
      assert (Q' <> B0') by (intro; apply HNBet; Between).
(* Goal: @Cong Tn B0' Q' A' B' *)
      assert (A' <> B0') by (intro; treat_equalities; auto).
(* Goal: @Cong Tn B0' Q' A' B' *)
      assert (HOut3 : Out B0' B' Q').
(* Goal: @Out Tn B0' B' Q' *)
(* Goal: @Cong Tn B0' Q' A' B' *)
       apply (l6_7 _ _ A'); [| apply l6_6]; apply bet_out; Between.
(* Goal: @Cong Tn B0' Q' A' B' *)
      assert (Hbet11 : Bet B0' B' Q').
(* Goal: @Bet Tn B0' B' Q' *)
(* Goal: @Cong Tn B0' Q' A' B' *)
        apply out2__bet; auto.
(* Goal: @Col Tn A0 A1 A *)
(* Goal: not (@Col Tn A0 A1 B0) *)
(* Goal: @Lt Tn A0 D A0 C *)
        apply not_bet_out; Col.
(* Goal: @Cong Tn B0' Q' A' B' *)
      apply (l2_11 _ B' _ _ Q'); Cong; eBetween.
    }
(* Goal: @Lt Tn A0 Q' A0 C *)
    assert (Hbet10 : Bet A0 D1 C) by eBetween.
(* Goal: @Lt Tn A0 Q' A0 C *)
    apply (cong2_lt__lt D1 C A0 C); Cong; [split|].
(* Goal: @Le Tn D1 C A0 C *)
(* Goal: not (@Cong Tn D1 C A0 C) *)
(* Goal: @Cong Tn D1 C A0 Q' *)
      destruct (l5_12_a A0 D1 C); auto.
(* Goal: not (@Cong Tn D1 C A0 C) *)
(* Goal: @Cong Tn D1 C A0 Q' *)
      intro; assert (D1 = A0) by (apply (between_cong C); Between; Cong); treat_equalities; Cong.
(* Goal: @Cong Tn D1 C A0 Q' *)
    apply (l2_11 _ C0 _ _ B0'); eBetween; apply cong_transitivity with A0 B0; Cong.
  }
(* Goal: False *)
  unfold archimedes_axiom in *.
(* Goal: False *)
  specialize Harchi with A0 D1 A0 C.
(* Goal: False *)
  destruct Harchi as [D [HG Hle]].
(* Goal: not (@Cong Tn P P C0 B0) *)
    intro; treat_equalities; auto.
(* Goal: False *)
  assert(HLt := HG).
(* Goal: False *)
  apply H in HLt.
(* Goal: False *)
  apply grad__le in HG.
(* Goal: False *)
  apply (le__nlt A0 C A0 D); auto.
Qed.

Lemma t22_19 :
  archimedes_axiom ->
  forall A B C D, Saccheri A B C D -> ~ Obtuse A B C.
Proof.
(* Goal: forall (_ : @archimedes_axiom Tn) (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D), not (@Obtuse Tn A B C) *)
  intros archi A B C D HSac HObt.
(* Goal: False *)
  assert (H := t22_18 archi _ _ _ _ (sac_perm _ _ _ _ HSac)).
(* Goal: False *)
  apply H.
  apply lt_left_comm; apply <- lt_sac__obtuse; auto.
Qed.

Lemma archi__obtuse_case_elimination :
  archimedes_axiom ->
  ~ hypothesis_of_obtuse_saccheri_quadrilaterals.
Proof.
(* Goal: forall _ : @archimedes_axiom Tn, not (@hypothesis_of_obtuse_saccheri_quadrilaterals Tn) *)
  intros archi obtuse.
(* Goal: False *)
  destruct ex_saccheri as [A [B [C [D HSac]]]].
(* Goal: False *)
  absurd(Obtuse A B C).
(* Goal: not (@Obtuse Tn A B C) *)
(* Goal: @Obtuse Tn A B C *)
    apply t22_19 with D; trivial.
(* Goal: @Obtuse Tn A B C *)
    apply obtuse with D; trivial.
Qed.

Lemma t22_23_aux :
  forall A B C M N L,
    ~ Col A M N -> Per B C A -> A <> C -> Midpoint M A B ->
    Per M N A -> Col A C N ->
    Midpoint M N L -> Bet A N C /\ Lambert N L B C /\ Cong B L A N.
Proof.
(* Goal: forall (A B C M N L : @Tpoint Tn) (_ : not (@Col Tn A M N)) (_ : @Per Tn B C A) (_ : not (@eq (@Tpoint Tn) A C)) (_ : @Midpoint Tn M A B) (_ : @Per Tn M N A) (_ : @Col Tn A C N) (_ : @Midpoint Tn M N L), and (@Bet Tn A N C) (and (@Lambert Tn N L B C) (@Cong Tn B L A N)) *)
  intros A B C M N L HNCol HPerC HAC HM HPerN HColN HN.
(* Goal: and (@Bet Tn A N C) (and (@Lambert Tn N L B C) (@Cong Tn B L A N)) *)
  assert_diffs.
(* Goal: and (@Bet Tn A N C) (and (@Lambert Tn N L B C) (@Cong Tn B L A N)) *)
  assert (HBet : Bet A N C) by (apply per23_preserves_bet with M B; Perp; Col; Between).
(* Goal: and (@Bet Tn A N C) (and (@Lambert Tn N L B C) (@Cong Tn B L A N)) *)
  destruct (l11_49 A M N B M L) as [HCong1 [HCongA1 HCongA2]]; auto with cong.
(* Goal: @CongA Tn A M N B M L *)
(* Goal: and (@Bet Tn A N C) (and (@Lambert Tn N L B C) (@Cong Tn B L A N)) *)
    apply l11_14; Between.
(* Goal: and (@Bet Tn A N C) (and (@Lambert Tn N L B C) (@Cong Tn B L A N)) *)
  assert(B <> L) by (intro; treat_equalities; auto).
(* Goal: and (@Bet Tn A N C) (and (@Lambert Tn N L B C) (@Cong Tn B L A N)) *)
  repeat split; Cong.
  - intro; treat_equalities; apply HNCol; ColR.
  - intro; treat_equalities; apply H6.
(* Goal: @Col Tn A0 A1 A *)
(* Goal: not (@Col Tn A0 A1 B0) *)
(* Goal: @Lt Tn A0 D A0 C *)
    apply (l6_21 A M N M); Col.
(* Goal: @Col Tn N M B *)
    apply col_permutation_3, cop_per2__col with A; Col; Cop.
  - apply per_col with A; Col.
(* Goal: @Per Tn L N A *)
    apply l8_2, per_col with M; Col; Perp.
  - apply l8_2, per_col with A; Col.
  - apply l11_17 with M N A; auto.
(* Goal: @CongA Tn M N A N L B *)
    apply (out_conga M N A M L B); auto; try (apply out_trivial; auto).
(* Goal: @Out Tn L M N *)
    apply bet_out; Between.
  - apply coplanar_perm_16, col_cop__cop with M; Col.
(* Goal: @Coplanar Tn B C N M *)
    apply coplanar_perm_12, col_cop__cop with A; Col; Cop.
Qed.

Lemma t22_23 :
  ~ hypothesis_of_obtuse_saccheri_quadrilaterals ->
  forall A B C M N L,
    ~ Col A M N -> Per B C A -> A <> C -> Midpoint M A B ->
    Per M N A -> Col A C N -> Midpoint M N L ->
    Bet A N C /\ Le N C A N /\ Le L N B C.
Proof.
(* Goal: forall (_ : not (@hypothesis_of_obtuse_saccheri_quadrilaterals Tn)) (A B C M N L : @Tpoint Tn) (_ : not (@Col Tn A M N)) (_ : @Per Tn B C A) (_ : not (@eq (@Tpoint Tn) A C)) (_ : @Midpoint Tn M A B) (_ : @Per Tn M N A) (_ : @Col Tn A C N) (_ : @Midpoint Tn M N L), and (@Bet Tn A N C) (and (@Le Tn N C A N) (@Le Tn L N B C)) *)
  intros HNob A B C M N L HNCol HPerC HAC HM HPerN HColN HN.
(* Goal: and (@Bet Tn A N C) (and (@Le Tn N C A N) (@Le Tn L N B C)) *)
  destruct (t22_23_aux A B C M N L) as [HBet [HLam HCong]]; auto.
(* Goal: @Midpoint Tn B A B' *)
  split; auto.
(* Goal: and (@Le Tn N C A N) (@Le Tn L N B C) *)
  assert (HLBC : ~ Obtuse L B C) by (intro; apply HNob, (lam_obtuse__oah N L B C); trivial).
(* Goal: and (@Le Tn N C A N) (@Le Tn L N B C) *)
  assert (Hos1 : OS N L B C) by (apply lam__os; trivial).
(* Goal: and (@Le Tn N C A N) (@Le Tn L N B C) *)
  assert (Hos2 : OS N C B L) by (apply lam__os, lam_perm; trivial).
(* Goal: and (@Le Tn N C A N) (@Le Tn L N B C) *)
  unfold Lambert in HLam; spliter.
(* Goal: and (@Le Tn N C A N) (@Le Tn L N B C) *)
  destruct (angle_partition L B C) as [HAcute | [HPer | HObtuse]]; trivial; [ | | exfalso; auto].
  - split; apply lt__le; [apply (cong2_lt__lt N C B L); Cong | ].
(* Goal: @Lt Tn N C B L *)
(* Goal: @Lt Tn L N B C *)
      apply lta_os_per2__lt; Perp; Side; apply lta_left_comm, acute_per__lta; auto.
(* Goal: @Lt Tn L N B C *)
    apply lt_left_comm, lta_os_per2__lt; Side; apply acute_per__lta; auto.
  - split; apply cong__le; [apply cong_transitivity with B L; trivial | apply cong_left_commutativity];
    apply conga_per2_os__cong; Perp; Side; apply l11_16; Perp.
Qed.

(** For every n, 2^n times B0C0 is lower than or equal to BnCn *)
(** B0 is introduced twice for the induction tactic to work properly *)
Lemma t22_24_aux :
  ~ hypothesis_of_obtuse_saccheri_quadrilaterals ->
  forall A B0 B00 C0 B C E,
    ~ Col A B0 C0 -> Perp A C0 B0 C0 -> B0 = B00 ->
    GradExp2 A B0 B B00 C0 E -> Perp A C0 B C -> Col A C0 C ->
    Le B0 E B C.
Proof.
(* Goal: forall (_ : not (@hypothesis_of_obtuse_saccheri_quadrilaterals Tn)) (A B0 B00 C0 B C E : @Tpoint Tn) (_ : not (@Col Tn A B0 C0)) (_ : @Perp Tn A C0 B0 C0) (_ : @eq (@Tpoint Tn) B0 B00) (_ : @GradExp2 Tn A B0 B B00 C0 E) (_ : @Perp Tn A C0 B C) (_ : @Col Tn A C0 C), @Le Tn B0 E B C *)
  intros HNob A B0 B00 C0 B C E HNCol HPerp0 Heq HGE.
(* Goal: forall (_ : @Perp Tn A C0 B C) (_ : @Col Tn A C0 C), @Le Tn B0 E B C *)
  revert C.
(* Goal: forall (C : @Tpoint Tn) (_ : @Perp Tn A C0 B C) (_ : @Col Tn A C0 C), @Le Tn B0 E B C *)
  induction HGE; rename B into B0; rename D into B00; rename E into C0; subst B00.
(* Goal: forall (C : @Tpoint Tn) (_ : @Perp Tn A C0 B0 C) (_ : @Col Tn A C0 C), @Le Tn B0 C0 B0 C *)
(* Goal: forall (C : @Tpoint Tn) (_ : @Perp Tn A C0 C' C) (_ : @Col Tn A C0 C), @Le Tn B0 F' C' C *)
    intros C HPerp HCol; assert (C = C0) by (apply (l8_18_uniqueness A C0 B0); Col); subst C; Le.
(* Goal: forall (C : @Tpoint Tn) (_ : @Perp Tn A C0 C' C) (_ : @Col Tn A C0 C), @Le Tn B0 F' C' C *)
  rename C into B; rename C' into B'; rename F into E; rename F' into E'.
(* Goal: forall (C : @Tpoint Tn) (_ : @Perp Tn A C0 B' C) (_ : @Col Tn A C0 C), @Le Tn B0 E' B' C *)
  intros C' HPerp' HCol'.
(* Goal: @Le Tn B0 E' B' C' *)
  apply gradexp2__gradexp123, gradexp__grad, grad__bet in HGE.
(* Goal: @Le Tn B0 E' B' C' *)
  destruct (l8_18_existence A C0 B) as [C [HCol HPerp]].
(* Goal: not (@Col Tn A C0 B) *)
(* Goal: @Le Tn B0 E' B' C' *)
    intro; assert_diffs; apply HNCol; ColR.
(* Goal: @Le Tn B0 E' B' C' *)
  assert (HLe : Le B0 E B C) by (apply IHHGE; trivial).
(* Goal: @Le Tn B0 E' B' C' *)
  clear IHHGE.
(* Goal: @Le Tn B0 E' B' C' *)
  destruct (symmetric_point_construction C B) as [D HD].
(* Goal: @Le Tn B0 E' B' C' *)
  apply le_transitivity with D C.
(* Goal: @Le Tn B0 E' D C *)
(* Goal: @Le Tn D C B' C' *)
    apply bet2_le2__le1346 with E B; Between; apply (l5_6 B0 E B C); auto with cong.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
  assert (HAC : A <> C).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
  { intro; subst C; assert_diffs; assert (A = C0); auto.
(* Goal: @Col Tn A0 A1 A *)
(* Goal: not (@Col Tn A0 A1 B0) *)
(* Goal: @Lt Tn A0 D A0 C *)
    apply (l8_18_uniqueness A C0 B0); Col.
(* Goal: @Col Tn A0 A1 A *)
(* Goal: not (@Col Tn A0 A1 B0) *)
(* Goal: @Lt Tn A0 D A0 C *)
    apply perp_right_comm, perp_col1 with B; Perp; Col.
  }
(* Goal: @Le Tn D C B' C' *)
  assert (HAC' : A <> C').
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
  { intro; subst C'; assert_diffs; assert (A = C0); auto.
(* Goal: @Col Tn A0 A1 A *)
(* Goal: not (@Col Tn A0 A1 B0) *)
(* Goal: @Lt Tn A0 D A0 C *)
    apply (l8_18_uniqueness A C0 B0); Col.
(* Goal: @Perp Tn A C0 B0 A *)
    apply perp_right_comm, perp_col1 with B'; Perp; ColR.
  }
(* Goal: @Le Tn D C B' C' *)
  assert (HPer : Per A C B) by (apply perp_per_1; auto; apply perp_left_comm, perp_col with C0; trivial).
(* Goal: and (@Bet Tn A N C) (and (@Lambert Tn N L B C) (@Cong Tn B L A N)) *)
  destruct (t22_23 HNob A B' C' B C D) as [_ []]; Perp; assert_diffs.
  - apply per_not_col in HPer; Col.
  - apply perp_per_1; auto; apply perp_col1 with C0; Perp.
  - split; auto.
  - ColR.
Qed.

(** For every n, it is possible to get Bn and Cn *)
Lemma t22_24_aux1 : forall A B0 C0 E,
  ~ Col A B0 C0 -> Perp A C0 B0 C0 -> GradExp B0 C0 E ->
  exists B C, GradExp2 A B0 B B0 C0 E /\ Perp A C0 B C /\ Col A C0 C.
Proof.
(* Goal: forall (A B0 C0 E : @Tpoint Tn) (_ : not (@Col Tn A B0 C0)) (_ : @Perp Tn A C0 B0 C0) (_ : @GradExp Tn B0 C0 E), @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp2 Tn A B0 B B0 C0 E) (and (@Perp Tn A C0 B C) (@Col Tn A C0 C)))) *)
  intros A B0 C0 E HNCol HPerp0 HGE.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp2 Tn A B0 B B0 C0 E) (and (@Perp Tn A C0 B C) (@Col Tn A C0 C)))) *)
  induction HGE; rename A0 into B0; rename B into C0.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp2 Tn A B0 B B0 C0 C0) (and (@Perp Tn A C0 B C) (@Col Tn A C0 C)))) *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp2 Tn A B0 B B0 C0 C') (and (@Perp Tn A C0 B C) (@Col Tn A C0 C)))) *)
    exists B0; exists C0; repeat (split; Col); apply gradexp2_init.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp2 Tn A B0 B B0 C0 C') (and (@Perp Tn A C0 B C) (@Col Tn A C0 C)))) *)
  rename C into E; rename C' into E'.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp2 Tn A B0 B B0 C0 E') (and (@Perp Tn A C0 B C) (@Col Tn A C0 C)))) *)
  destruct IHHGE as [B [C [HGE2 [HPerp HCol]]]]; trivial.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp2 Tn A B0 B B0 C0 E') (and (@Perp Tn A C0 B C) (@Col Tn A C0 C)))) *)
  destruct (segment_construction A B A B) as [B' [HBet HCong]].
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp2 Tn A B0 B B0 C0 E') (and (@Perp Tn A C0 B C) (@Col Tn A C0 C)))) *)
  exists B'.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp2 Tn A B0 B' B0 C0 E') (and (@Perp Tn A C0 B' C) (@Col Tn A C0 C))) *)
  destruct (l8_18_existence A C0 B') as [C' [HCol' HPerp']].
(* Goal: not (@Col Tn A C0 B) *)
(* Goal: @Le Tn B0 E' B' C' *)
    apply gradexp2__gradexp123, gradexp__grad, grad__bet in HGE2; intro; assert_diffs; apply HNCol; ColR. 
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp2 Tn A B0 B' B0 C0 E') (and (@Perp Tn A C0 B' C) (@Col Tn A C0 C))) *)
  exists C'; repeat (split; trivial); apply gradexp2_stab with B E; Cong.
Qed.

Lemma t22_24 : archimedes_axiom -> aristotle_s_axiom.
Proof.
(* Goal: forall _ : @archimedes_axiom Tn, @aristotle_s_axiom Tn *)
  intros Harchi P Q D A B0 HNCol HACute0.
(* Goal: @Col Tn A0 A1 A *)
(* Goal: not (@Col Tn A0 A1 B0) *)
(* Goal: @Lt Tn A0 D A0 C *)
  destruct (l8_18_existence A D B0) as [C0 [HColD HPerpD]]; Col.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
  assert (HAC0 : A <> C0) by (intro; subst C0; apply (acute_not_per D A B0); Perp).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
  assert (HNCol0 : ~ Col A B0 C0) by (intro; apply HNCol; ColR).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
  assert (HPerp0 := perp_col A D B0 C0 C0 HAC0 HPerpD HColD).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
  elim (eq_dec_points P Q); intro HPQ.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
  { subst Q; exists C0; exists B0; split; assert_diffs.
(* Goal: @Out Tn A D C0 *)
(* Goal: and (@Out Tn A B0 B0) (and (@Per Tn A C0 B0) (@Lt Tn P P C0 B0)) *)
      apply l6_6, acute_col_perp__out with B0; trivial; apply acute_sym; trivial.
(* Goal: @Lt Tn P Q P Q' *)
(* Goal: @Le Tn P Q' C B *)
    split.
(* Goal: @Out Tn A B0 B0 *)
(* Goal: and (@Per Tn A C0 B0) (@Lt Tn P P C0 B0) *)
      apply out_trivial; auto.
(* Goal: and (@Per Tn A C0 B0) (@Lt Tn P P C0 B0) *)
    repeat split; Perp; Le.
(* Goal: not (@Cong Tn P P C0 B0) *)
    intro; treat_equalities; auto.
  }
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
  destruct (segment_construction P Q P Q) as [Q' [HBetQ HCongQ]].
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
  destruct (reach__ex_gradexp_le B0 C0 P Q') as [E [HGE HLe]].
(* Goal: @Reach Tn B0 C0 P Q' *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
    assert_diffs; apply Harchi; trivial.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
  destruct (t22_24_aux1 A B0 C0 E) as [B [C [HGE2 [HPerp HCol]]]]; trivial.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
  assert(HOut : Out A B0 B).
(* Goal: @Out Tn A B0 B *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
    apply gradexp2__gradexp123, gradexp__grad, grad__bet in HGE2; assert_diffs; apply bet_out; auto.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
  assert(HAcute : Acute D A B).
(* Goal: @Acute Tn D A B *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
    apply (acute_conga__acute D A B0); trivial.
(* Goal: @Out Tn A B0 B0 *)
(* Goal: and (@Per Tn A C0 B0) (@Lt Tn P P C0 B0) *)
    assert_diffs; apply (out_conga D A B0 D A B0); CongA; apply out_trivial; auto.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
  assert (HAC : A <> C) .
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A D X) (and (@Out Tn A B0 Y) (and (@Per Tn A X Y) (@Lt Tn P Q X Y))))) *)
    intro; subst C; assert_diffs; apply (acute_not_per D A B); trivial.
(* Goal: @Col Tn A0 A1 A *)
(* Goal: not (@Col Tn A0 A1 B0) *)
(* Goal: @Lt Tn A0 D A0 C *)
    apply perp_per_1; auto; apply perp_col with C0; Col.
(* Goal: @Lt Tn P Q P Q' *)
(* Goal: @Le Tn P Q' C B *)
  exists C; exists B; split.
(* Goal: @Out Tn A D C *)
(* Goal: and (@Out Tn A B0 B) (and (@Per Tn A C B) (@Lt Tn P Q C B)) *)
    assert_diffs; apply l6_6, acute_col_perp__out with B; [apply acute_sym; trivial|ColR|apply perp_col with C0; Col].
(* Goal: @Lt Tn P Q P Q' *)
(* Goal: @Le Tn P Q' C B *)
  split; trivial; split.
(* Goal: @Per Tn A C B *)
(* Goal: @Lt Tn P Q C B *)
    apply perp_per_1; auto; apply perp_left_comm, perp_col with C0; trivial.
(* Goal: @Lt Tn P Q C B *)
  apply le3456_lt__lt with P Q'.
(* Goal: @Lt Tn P Q P Q' *)
(* Goal: @Le Tn P Q' C B *)
  split.
(* Goal: @Le Tn P Q P Q' *)
(* Goal: not (@Cong Tn P Q P Q') *)
(* Goal: @Le Tn P Q' C B *)
    apply bet__le1213; trivial.
(* Goal: not (@Cong Tn P Q P Q') *)
(* Goal: @Le Tn P Q' C B *)
    intro; assert (Q = Q'); treat_equalities; auto.
(* Goal: @eq (@Tpoint Tn) Q Q' *)
(* Goal: @Le Tn P Q' C B *)
    apply between_cong with P; trivial.
(* Goal: @Le Tn P Q' C B *)
  apply le_transitivity with B0 E; trivial.
(* Goal: @Le Tn B0 E C B *)
  apply le_right_comm.
(* Goal: @Le Tn B0 E B C *)
  apply t22_24_aux with A B0 C0; trivial.
(* Goal: not (@hypothesis_of_obtuse_saccheri_quadrilaterals Tn) *)
  apply archi__obtuse_case_elimination; trivial.
Qed.


End Archimedes.