Require Import GeoCoq.Axioms.continuity_axioms.
Require Import GeoCoq.Meta_theory.Continuity.archimedes.
Require Import GeoCoq.Tarski_dev.Annexes.suma.
Require Import GeoCoq.Tarski_dev.Ch12_parallel.

Section Archimedes_for_angles.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma grada_distincts : forall A B C D E F,
  GradA A B C D E F ->
  A <> B /\ C <> B /\ D <> E /\ F <> E.
Proof.
(* Goal: forall (P Q R : @Tpoint Tn) (_ : @GradA Tn A B C P Q R), @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn P Q R S T U))))) *)
  induction 1.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C B)) (and (not (@eq (@Tpoint Tn) D E)) (not (@eq (@Tpoint Tn) F E)))) *)
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C B)) (and (not (@eq (@Tpoint Tn) G H)) (not (@eq (@Tpoint Tn) I H)))) *)
    assert_diffs; repeat split; trivial.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C B)) (and (not (@eq (@Tpoint Tn) G H)) (not (@eq (@Tpoint Tn) I H)))) *)
  apply suma_distincts in H2; spliter; repeat split; auto.
Qed.

Lemma conga2_grada__grada : forall A B C D E F A' B' C' D' E' F',
  GradA A B C D E F ->
  CongA A B C A' B' C' -> CongA D E F D' E' F' ->
  GradA A' B' C' D' E' F'.
Proof.
(* Goal: forall (A B C D E F A' B' C' D' E' F' : @Tpoint Tn) (_ : @GradA Tn A B C D E F) (_ : @CongA Tn A B C A' B' C') (_ : @CongA Tn D E F D' E' F'), @GradA Tn A' B' C' D' E' F' *)
  intros A B C D E F A' B' C' D' E' F' HGA.
(* Goal: forall (_ : @CongA Tn A B C A' B' C') (_ : @CongA Tn D E F D' E' F'), @GradA Tn A' B' C' D' E' F' *)
  revert A' B' C' D' E' F'.
(* Goal: forall (A' B' C' D' E' F' : @Tpoint Tn) (_ : @CongA Tn A B C A' B' C') (_ : @CongA Tn D E F D' E' F'), @GradA Tn A' B' C' D' E' F' *)
  induction HGA; intros A' B' C' D' E' F' Hconga1 Hconga2.
(* Goal: @GradA Tn A' B' C' D' E' F' *)
(* Goal: @GradA Tn A' B' C' D' E' F' *)
    apply grada_init, conga_trans with D E F; trivial; apply conga_trans with A B C; CongA.
(* Goal: or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)) *)
  suma.assert_diffs.
(* Goal: @GradA Tn A' B' C' D' E' F' *)
  assert (Hconga3 : CongA D E F D E F) by CongA.
(* Goal: @GradA Tn A' B' C' D' E' F' *)
  apply grada_stab with D E F.
(* Goal: @GradA Tn A' B' C' D E F *)
(* Goal: @SAMS Tn D E F A' B' C' *)
(* Goal: @SumA Tn D E F A' B' C' D' E' F' *)
    apply (IHHGA A' B' C' D E F); trivial.
(* Goal: @SAMS Tn D E F A' B' C' *)
(* Goal: @SumA Tn D E F A' B' C' D' E' F' *)
    apply (conga2_sams__sams D E F A B C); trivial.
(* Goal: @SumA Tn D E F A' B' C' D' E' F' *)
  apply (conga3_suma__suma D E F A B C G H I); trivial.
Qed.

Lemma grada__lea : forall A B C D E F, GradA A B C D E F -> LeA A B C D E F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @GradA Tn A B C D E F), @LeA Tn A B C D E F *)
  intros A B C D E F.
(* Goal: forall (P Q R : @Tpoint Tn) (_ : @GradA Tn A B C P Q R), @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn P Q R S T U))))) *)
  induction 1.
(* Goal: @LeA Tn A B C D E F *)
(* Goal: @LeA Tn A B C G H I *)
    Lea.
(* Goal: @LeA Tn A B C G H I *)
  apply lea_trans with D E F; trivial.
(* Goal: @LeA Tn D0 E0 F0 G H I *)
(* Goal: @GradA Tn A B C K0 L0 M0 *)
  apply sams_suma__lea123789 with A B C; trivial.
Qed.

Lemma grada_out__out : forall A B C D E F,
  Out E D F -> GradA A B C D E F ->
  Out B A C.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @Out Tn E D F) (_ : @GradA Tn A B C D E F), @Out Tn B A C *)
  intros A B C D E F Hout HGA.
(* Goal: @Out Tn B A C *)
  apply out_lea__out with D E F; trivial.
(* Goal: @LeA Tn A B C D E F *)
  apply grada__lea; trivial.
Qed.

Lemma grada2_sams_suma__grada : forall A B C D E F G H I K L M,
  GradA A B C D E F -> GradA A B C G H I ->
  SAMS D E F G H I -> SumA D E F G H I K L M ->
  GradA A B C K L M.
Proof.
(* Goal: forall (A B C D E F G H I K L M : @Tpoint Tn) (_ : @GradA Tn A B C D E F) (_ : @GradA Tn A B C G H I) (_ : @SAMS Tn D E F G H I) (_ : @SumA Tn D E F G H I K L M), @GradA Tn A B C K L M *)
  intros A B C D E F G H I K L M HGA1 HGA2 HIsi.
(* Goal: forall _ : @SumA Tn D E F G H I K L M, @GradA Tn A B C K L M *)
  revert K L M.
(* Goal: forall _ : not (@SAMS Tn D E F G H I), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (not (@SAMS Tn P Q R A B C))))) *)
  induction HGA2.
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
  { rename H into HConga; rename D0 into G; rename E0 into H; rename F0 into I.
(* Goal: forall (K L M : @Tpoint Tn) (_ : @SumA Tn D E F G H I K L M), @GradA Tn A B C K L M *)
    intros K L M HSuma.
(* Goal: or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)) *)
    suma.assert_diffs.
(* Goal: @GradA Tn A B C K L M *)
    apply (conga2_sams__sams D E F G H I D E F A B C) in HIsi; CongA.
(* Goal: @GradA Tn A B C K L M *)
    apply (conga3_suma__suma D E F G H I K L M D E F A B C K L M) in HSuma; CongA.
(* Goal: @GradA Tn A B C K L M *)
    apply grada_stab with D E F; trivial.
  }
(* Goal: forall (K L M : @Tpoint Tn) (_ : @SumA Tn D E F G H I K L M), @GradA Tn A B C K L M *)
  assert (Hd1 := sams_distincts D0 E0 F0 A B C H0); assert (Hd2 := sams_distincts D E F G H I HIsi); spliter.
(* Goal: forall (K L M : @Tpoint Tn) (_ : @SumA Tn D E F G H I K L M), @GradA Tn A B C K L M *)
  destruct (ex_suma D E F D0 E0 F0) as [K [L [M HSuma]]]; auto.
(* Goal: forall (K L M : @Tpoint Tn) (_ : @SumA Tn D E F G H I K L M), @GradA Tn A B C K L M *)
  intros K0 L0 M0 HSuma2.
(* Goal: @GradA Tn A B C K0 L0 M0 *)
  assert (HIsi2 : SAMS D E F D0 E0 F0).
(* Goal: @LeA Tn A B C D E F *)
(* Goal: @LeA Tn A B C G H I *)
    apply sams_lea2__sams with D E F G H I; Lea.
(* Goal: @LeA Tn D0 E0 F0 G H I *)
(* Goal: @GradA Tn A B C K0 L0 M0 *)
    apply sams_suma__lea123789 with A B C; trivial.
(* Goal: @GradA Tn A B C K0 L0 M0 *)
  apply grada_stab with K L M.
(* Goal: @GradA Tn A B C K L M *)
(* Goal: @SAMS Tn K L M A B C *)
(* Goal: @SumA Tn K L M A B C K0 L0 M0 *)
    apply IHHGA2; trivial.
(* Goal: @SAMS Tn K L M A B C *)
(* Goal: @SumA Tn K L M A B C K0 L0 M0 *)
    apply sams_assoc_2 with D E F D0 E0 F0 G H I; trivial.
(* Goal: @SumA Tn K L M A B C K0 L0 M0 *)
  apply suma_assoc_2 with D E F D0 E0 F0 G H I; trivial.
Qed.

Lemma gradaexp__grada : forall A B C D E F,
  GradAExp A B C D E F -> GradA A B C D E F.
Proof.
(* Goal: forall (A B C P Q R : @Tpoint Tn) (_ : @GradA Tn A B C P Q R), @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn P Q R S T U))))) *)
  intros A B C.
(* Goal: forall (D E F : @Tpoint Tn) (_ : @GradAExp Tn A B C D E F), @GradA Tn A B C D E F *)
  induction 1; [apply grada_init | apply grada2_sams_suma__grada with D E F D E F]; trivial.
Qed.

Lemma acute_archi_aux : forall O A B C D E,
  Per O A B -> O <> A -> B <> A -> C <> D -> D <> E ->
  Bet A C D -> Bet C D E -> Bet D E B -> CongA C O D D O E ->
  Lt C D D E.
Proof.
(* Goal: forall (O A B C D E : @Tpoint Tn) (_ : @Per Tn O A B) (_ : not (@eq (@Tpoint Tn) O A)) (_ : not (@eq (@Tpoint Tn) B A)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@eq (@Tpoint Tn) D E)) (_ : @Bet Tn A C D) (_ : @Bet Tn C D E) (_ : @Bet Tn D E B) (_ : @CongA Tn C O D D O E), @Lt Tn C D D E *)
  intros O A B C D E HPer HOA HBA HCD HDE HBet1 HBet2 HBet3 HCongA.
(* Goal: @Obtuse Tn P Q R *)
  assert_diffs.
(* Goal: @Lt Tn C D D E *)
  assert (HNCol1 : ~ Col O A B) by (apply per_not_col; auto).
(* Goal: @Lt Tn C D D E *)
  assert (HNCol2 : ~ Col O A D).
(* Goal: not (@Col Tn O A D) *)
(* Goal: @Lt Tn C D D E *)
    intro; elim (eq_dec_points A C); intro; assert_cols; treat_equalities; apply HNCol1; ColR.
(* Goal: @Lt Tn C D D E *)
  destruct (angle_construction_1 A D O O D E) as [P [HP1 HP2]]; Col.
(* Goal: not (@Col Tn O D C) *)
(* Goal: @CongA Tn D O C D O F *)
(* Goal: @CongA Tn O D C O D F *)
(* Goal: @Lt Tn C D D E *)
    intro; apply HNCol2; ColR.
(* Goal: @Lt Tn C D D E *)
  assert (HAcute : Acute A D O).
(* Goal: @Acute Tn A D O *)
(* Goal: @Lt Tn C D D E *)
    apply l11_43_aux; Col; left; apply l8_2, per_col with B; auto; ColR.
(* Goal: @Lt Tn C D D E *)
  assert (HF : InAngle P O D E).
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
  { apply lea_in_angle; Side.
(* Goal: @LeA Tn O D P O D E *)
    apply (l11_30 A D O E D O); CongA.
(* Goal: @LeA Tn A D O E D O *)
    destruct (acute_chara A D O E) as [HD HI]; eBetween.
(* Goal: @LeA Tn A D O E D O *)
    apply lta__lea, HD, HAcute.
  }
(* Goal: @Lt Tn C D D E *)
  destruct HF as [_ [_ [HDP [F [HBet4 [Heq|HOut]]]]]].
(* Goal: @Lt Tn C D D E *)
(* Goal: @Lt Tn C D D E *)
    exfalso; subst F; apply HNCol2; ColR.
(* Goal: @Obtuse Tn P Q R *)
  assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
  apply l6_6 in HOut.
(* Goal: @Lt Tn C D D E *)
  assert (HCongA1 : CongA A D O O D F).
(* Goal: @CongA Tn A D O O D F *)
(* Goal: @Lt Tn C D D E *)
    apply (out_conga A D O O D P); trivial; apply out_trivial; auto.
(* Goal: @Lt Tn C D D E *)
  assert (HCongA2 : CongA O D C A D O).
(* Goal: @CongA Tn O D C A D O *)
(* Goal: @Lt Tn C D D E *)
    elim (eq_dec_points A C); intro.
(* Goal: @CongA Tn O D C A D O *)
(* Goal: @CongA Tn O D C A D O *)
(* Goal: @Lt Tn C D D E *)
      treat_equalities; CongA.
(* Goal: @CongA Tn O D C A D O *)
(* Goal: @Lt Tn C D D E *)
    apply (out_conga O D C C D O); CongA; try (apply out_trivial; auto); apply bet_out; eBetween.
(* Goal: @Lt Tn C D D E *)
  clear dependent P.
(* Goal: @Lt Tn C D D E *)
  assert (HNCol3 : ~ Col O D F) by (apply (ncol_conga_ncol A D O); Col).
(* Goal: @Obtuse Tn P Q R *)
  assert_diffs.
(* Goal: @Lt Tn C D D E *)
  destruct (l11_50_1 O D C O D F) as [HCong1 [HCong2 HCongA3]]; Cong.
(* Goal: not (@Col Tn O D C) *)
(* Goal: @CongA Tn D O C D O F *)
(* Goal: @CongA Tn O D C O D F *)
(* Goal: @Lt Tn C D D E *)
    intro; apply HNCol2; ColR.
(* Goal: @CongA Tn D O C D O F *)
(* Goal: @CongA Tn O D C O D F *)
(* Goal: @Lt Tn C D D E *)
    apply (out_conga D O C D O E); CongA; try (apply out_trivial; auto); apply l6_6, bet_out; auto.
(* Goal: @CongA Tn O D C O D F *)
(* Goal: @Lt Tn C D D E *)
    apply conga_trans with A D O; trivial.
(* Goal: @Lt Tn C D D E *)
  apply (cong2_lt__lt D F D E); Cong.
(* Goal: @Lt Tn D F D E *)
  assert (HNCol4 : ~ Col E D F).
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
  { intro; elim (eq_dec_points E F); intro; [|apply HNCol3; ColR].
(* Goal: @Col Tn A0 O A1 *)
    treat_equalities.
(* Goal: False *)
    apply (acute_not_per A D O); trivial.
(* Goal: @Per Tn A D O *)
    apply l8_2, per_col with C; Col.
(* Goal: @Per Tn O D C *)
    exists E; repeat split; Cong.
  }
(* Goal: @Obtuse Tn P Q R *)
  assert_diffs.
(* Goal: @Lt Tn D F D E *)
  apply l11_44_2_b; trivial.
(* Goal: @LtA Tn D E F D F E *)
  apply lta_trans with F D O.
  - destruct (l11_41 D E O C) as [Hlta1 Hlta2]; Between.
(* Goal: not (@Col Tn D E O) *)
(* Goal: @LtA Tn D E F F D O *)
      intro; apply HNCol3; ColR.
    apply (conga_preserves_lta D E O O D C); trivial;
    [apply (out_conga D E F D E F)|apply (out_conga O D A F D O)]; CongA;
    try (apply out_trivial; auto).
(* Goal: @Out Tn E F O *)
(* Goal: @Out Tn D A C *)
      apply bet_out; Between.
(* Goal: @Out Tn D A C *)
    apply l6_6, bet_out; eBetween.
  - destruct (l11_41 F O D E); Col.
Qed.

Lemma acute_archi_aux1 : forall O A0 A1 B P Q R,
  Per O A0 B -> B <> A0 -> Bet A0 A1 B ->
  GradA A0 O A1 P Q R -> A0 <> A1 ->
  LeA A0 O B P Q R \/ exists A, Bet A0 A1 A /\ Bet A0 A B /\ CongA P Q R A0 O A.
Proof.
(* Goal: forall (O A0 A1 B P Q R : @Tpoint Tn) (_ : @Per Tn O A0 B) (_ : not (@eq (@Tpoint Tn) B A0)) (_ : @Bet Tn A0 A1 B) (_ : @GradA Tn A0 O A1 P Q R) (_ : not (@eq (@Tpoint Tn) A0 A1)), or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A1 A) (and (@Bet Tn A0 A B) (@CongA Tn P Q R A0 O A)))) *)
  intros O A0 A1 B P Q R HPer HBA0 HBet HGA HA0A1.
(* Goal: or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A1 A) (and (@Bet Tn A0 A B) (@CongA Tn P Q R A0 O A)))) *)
  assert (Hdiff := grada_distincts A0 O A1 P Q R HGA); spliter.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A0 O A1 P Q R) (or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P Q R A0 O A') (and (@Le Tn A0 E A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A'))))))))))))) *)
  assert (HNCol : ~ Col O A0 B) by (apply per_not_col; auto).
(* Goal: @Obtuse Tn P Q R *)
  assert_diffs.
(* Goal: or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A1 A) (and (@Bet Tn A0 A B) (@CongA Tn P Q R A0 O A)))) *)
  elim (lea_total A0 O B P Q R); auto.
(* Goal: forall _ : @LeA Tn P Q R A0 O B, or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A1 A) (and (@Bet Tn A0 A B) (@CongA Tn P Q R A0 O A)))) *)
  intro HLeA; right.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A1 A) (and (@Bet Tn A0 A B) (@CongA Tn P Q R A0 O A))) *)
  assert (HNCol2 : ~ Col P Q R).
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
  { intro HCol.
(* Goal: False *)
    assert (HBet1 : Bet P Q R).
(* Goal: @Bet Tn P Q R *)
(* Goal: False *)
      apply not_out_bet; trivial.
(* Goal: not (@Out Tn Q P R) *)
(* Goal: False *)
      intro HOut; assert (Out O A0 A1) by (apply grada_out__out with P Q R; trivial).
(* Goal: False *)
(* Goal: False *)
      apply HNCol; ColR.
(* Goal: False *)
    assert (Bet A0 O B); assert_cols; Col.
(* Goal: @Bet Tn A0 O B *)
    apply bet_lea__bet with P Q R; trivial.
  }
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A1 A) (and (@Bet Tn A0 A B) (@CongA Tn P Q R A0 O A))) *)
  destruct (angle_construction_1 P Q R A0 O B) as [C [Hconga HOS]]; Col.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A1 A) (and (@Bet Tn A0 A B) (@CongA Tn P Q R A0 O A))) *)
  assert (HA : InAngle C A0 O B).
(* Goal: @InAngle Tn C A0 O B *)
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A1 A) (and (@Bet Tn A0 A B) (@CongA Tn P Q R A0 O A))) *)
    apply lea_in_angle; Side; apply (l11_30 P Q R A0 O B); CongA.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A1 A) (and (@Bet Tn A0 A B) (@CongA Tn P Q R A0 O A))) *)
  destruct HA as [_ [_ [HCO [A [HA HUn]]]]].
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A1 A) (and (@Bet Tn A0 A B) (@CongA Tn P Q R A0 O A))) *)
  destruct HUn as [Heq|Hout].
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A1 A) (and (@Bet Tn A0 A B) (@CongA Tn P Q R A0 O A))) *)
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A1 A) (and (@Bet Tn A0 A B) (@CongA Tn P Q R A0 O A))) *)
    exfalso; treat_equalities; apply HNCol; Col.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A1 A) (and (@Bet Tn A0 A B) (@CongA Tn P Q R A0 O A))) *)
  exists A.
(* Goal: and (@Bet Tn A0 A1 A) (and (@Bet Tn A0 A B) (@CongA Tn P Q R A0 O A)) *)
  apply (out_conga P Q R A0 O C P R A0 A) in Hconga; try (apply out_trivial; auto); [|apply l6_6; trivial].
(* Goal: and (@Bet Tn A0 A1 A) (and (@Bet Tn A0 A B) (@CongA Tn P Q R A0 O A)) *)
  repeat (split; trivial).
(* Goal: @Bet Tn A0 A1 A *)
  elim (eq_dec_points A1 A).
(* Goal: forall _ : @eq (@Tpoint Tn) A1 A, @Bet Tn A0 A1 A *)
(* Goal: forall _ : not (@eq (@Tpoint Tn) A1 A), @Bet Tn A0 A1 A *)
    intro; subst A; Between.
(* Goal: forall _ : not (@eq (@Tpoint Tn) A1 A), @Bet Tn A0 A1 A *)
  intro HAA1.
(* Goal: @Bet Tn A0 A1 A *)
  apply (ncol_conga_ncol P Q R A0 O A) in HNCol2; trivial.
(* Goal: @Bet Tn A0 A1 A *)
  assert (HInangle : InAngle A1 A0 O A).
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
  { apply lea_in_angle.
(* Goal: @LeA Tn A B C D E F *)
      apply (l11_30 A0 O A1 P Q R); CongA; apply grada__lea; trivial.
(* Goal: @OS Tn A0 O A A1 *)
    apply out_one_side; auto.
(* Goal: @Obtuse Tn P Q R *)
    assert_diffs.
(* Goal: @Out Tn A0 A A1 *)
    apply l6_7 with B; [|apply l6_6]; apply bet_out; auto.
  }
(* Goal: @Bet Tn A0 A1 A *)
  destruct HInangle as [_ [_ [_ [X [HX1 HUn]]]]].
(* Goal: @Bet Tn A0 A1 A *)
  destruct HUn as [HX2|HX2].
(* Goal: @Bet Tn A0 A1 A *)
(* Goal: @Bet Tn A0 A1 A *)
    subst X; exfalso; Col.
(* Goal: @Bet Tn A0 A1 A *)
  elim (eq_dec_points X A1); intro.
(* Goal: @Bet Tn A0 A1 A *)
(* Goal: @Bet Tn A0 A1 A *)
    subst X; trivial.
(* Goal: @Bet Tn A0 A1 A *)
  exfalso; apply HNCol2; assert_diffs; ColR.
Qed.

Lemma acute_archi_aux2 : forall O A0 A1 B C,
  Per O A0 B -> O <> A0 -> B <> A0 ->
  Bet A0 A1 B -> A0 <> A1 -> Grad A0 A1 C ->
  exists P, exists Q, exists R, GradA A0 O A1 P Q R /\ (LeA A0 O B P Q R \/
  exists A', Bet A0 A1 A' /\ Bet A0 A' B /\ CongA P Q R A0 O A' /\ Le A0 C A0 A' /\
  exists A, Bet A0 A A' /\ CongA A O A' A0 O A1 /\ Le A0 A1 A A').
Proof.
(* Goal: forall (O A0 A1 B C : @Tpoint Tn) (_ : @Per Tn O A0 B) (_ : not (@eq (@Tpoint Tn) O A0)) (_ : not (@eq (@Tpoint Tn) B A0)) (_ : @Bet Tn A0 A1 B) (_ : not (@eq (@Tpoint Tn) A0 A1)) (_ : @Grad Tn A0 A1 C), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A0 O A1 P Q R) (or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P Q R A0 O A') (and (@Le Tn A0 C A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A'))))))))))))) *)
  intros O A0 A1 B E HPer HOA0 HBA0 HBet HA0A1 HG.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A0 O A1 P Q R) (or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P Q R A0 O A') (and (@Le Tn A0 E A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A'))))))))))))) *)
  assert (HNCol : ~ Col O A0 B) by (apply per_not_col; auto).
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A0 O A1 P Q R) (or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P Q R A0 O A') (and (@Le Tn A0 E A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A'))))))))))))) *)
  assert (HNCol1 : ~ Col A0 O A1) by (intro; apply HNCol; ColR).
(* Goal: @Obtuse Tn P Q R *)
  assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A0 O A1 P Q R) (or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P Q R A0 O A') (and (@Le Tn A0 E A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A'))))))))))))) *)
  induction HG; rename A into A0; rename B0 into A1.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A0 O A1 P Q R) (or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P Q R A0 O A') (and (@Le Tn A0 A1 A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A'))))))))))))) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A0 O A1 P Q R) (or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P Q R A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A'))))))))))))) *)
    exists A0; exists O; exists A1; split; [apply grada_init; CongA|].
(* Goal: or (@LeA Tn A0 O B A0 O A1) (@ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn A0 O A1 A0 O A') (and (@Le Tn A0 A1 A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A'))))))))) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A0 O A1 P Q R) (or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P Q R A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A'))))))))))))) *)
    right; exists A1; repeat (split; CongA); Between; Le.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A1) (and (@CongA Tn A O A1 A0 O A1) (@Le Tn A0 A1 A A1))) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A0 O A1 P Q R) (or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P Q R A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A'))))))))))))) *)
    exists A0; repeat (split; CongA); Between; Le.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A0 O A1 P Q R) (or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P Q R A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A'))))))))))))) *)
  destruct IHHG as [P [Q [R [HGA HUn]]]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A0 O A1 P Q R) (or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P Q R A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A'))))))))))))) *)
  destruct HUn as [HLea|HA'].
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A0 O A1 P Q R) (or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P Q R A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A'))))))))))))) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A0 O A1 P Q R) (or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P Q R A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A'))))))))))))) *)
    exists P; exists Q; exists R; split; trivial; left; trivial.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A0 O A1 P Q R) (or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P Q R A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A'))))))))))))) *)
  destruct HA' as [A' [HBet1' [HBet2' [HConga' [HLe' HA]]]]].
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A0 O A1 P Q R) (or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P Q R A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A'))))))))))))) *)
  destruct HA as [A [HBet1 [HConga HLe]]].
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A0 O A1 P Q R) (or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P Q R A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A'))))))))))))) *)
  assert (HIsi : SAMS P Q R A0 O A1).
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
  { apply sams_lea2__sams with A0 O B A0 O B.
    - apply acute__sams, l11_43_aux; Col.
    - apply (l11_30 A0 O A' A0 O B); CongA.
(* Goal: @LeA Tn A0 O A' A0 O B *)
      exists A'; assert_diffs; split; CongA.
(* Goal: @InAngle Tn A1 A0 O B *)
      repeat split; auto.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A0 X B) (or (@eq (@Tpoint Tn) X O) (@Out Tn O X A'))) *)
      exists A'; split; trivial.
(* Goal: or (@eq (@Tpoint Tn) A1 O) (@Out Tn O A1 A1) *)
      right; apply out_trivial; auto.
    - exists A1; split; CongA.
(* Goal: @InAngle Tn A1 A0 O B *)
      repeat split; auto.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A0 X B) (or (@eq (@Tpoint Tn) X O) (@Out Tn O X A1))) *)
      exists A1; split; trivial.
(* Goal: or (@eq (@Tpoint Tn) A1 O) (@Out Tn O A1 A1) *)
      right; apply out_trivial; auto.
  }
(* Goal: @Obtuse Tn P Q R *)
  assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A0 O A1 P Q R) (or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P Q R A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A'))))))))))))) *)
  destruct (ex_suma P Q R A0 O A1) as [P' [Q' [R' HSuma]]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A0 O A1 P Q R) (or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P Q R A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A'))))))))))))) *)
  assert (HGA' : GradA A0 O A1 P' Q' R') by (apply grada_stab with P Q R; trivial).
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A0 O A1 P Q R) (or (@LeA Tn A0 O B P Q R) (@ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P Q R A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A'))))))))))))) *)
  exists P'; exists Q'; exists R'; split; trivial.
(* Goal: or (@LeA Tn A0 O B P' Q' R') (@ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P' Q' R' A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A'))))))))) *)
  destruct (acute_archi_aux1 O A0 A1 B P' Q' R') as [HLea|HA'']; auto.
(* Goal: or (@LeA Tn A0 O B P' Q' R') (@ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P' Q' R' A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A'))))))))) *)
  right; destruct HA'' as [A'' [HBet1'' [HBet2'' HConga'']]].
(* Goal: @ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P' Q' R' A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A')))))))) *)
  assert (HNCol2 : ~ Col A O A') by (apply (ncol_conga_ncol A0 O A1); Col; CongA).
(* Goal: @ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P' Q' R' A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A')))))))) *)
  assert (HNCol3 : ~ Col A0 O A') by (intro; assert_diffs; apply HNCol; ColR).
(* Goal: @ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P' Q' R' A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A')))))))) *)
  assert (HNCol4 : ~ Col A' O A'').
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
  { intro HCol; apply HNCol1.
(* Goal: @Col Tn A0 O A1 *)
    elim (eq_dec_points A' A''); intro; [|ColR].
(* Goal: @Col Tn A0 O A1 *)
    treat_equalities.
(* Goal: @Col Tn A0 O A1 *)
    assert (HSuma2 : SumA A0 O A' A0 O A1 A0 O A').
(* Goal: @SumA Tn A0 O A' A0 O A1 A0 O A' *)
(* Goal: @Col Tn A0 O A1 *)
      apply (conga3_suma__suma P Q R A0 O A1 P' Q' R'); CongA.
(* Goal: @Col Tn A0 O A1 *)
    apply sams_suma__out546 in HSuma2; Col.
(* Goal: @SAMS Tn A0 O A' A0 O A1 *)
    apply (conga2_sams__sams P Q R A0 O A1); CongA.
  }
(* Goal: @ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P' Q' R' A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A')))))))) *)
  assert (HNCol5 : ~ Col A0 O A'') by (intro; assert_diffs; apply HNCol4; ColR).
(* Goal: @ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P' Q' R' A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A')))))))) *)
  assert (HBet4 : Bet A0 A' A'').
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
  { apply col_two_sides_bet with O.
(* Goal: @Col Tn A' A0 A'' *)
(* Goal: @TS Tn A' O A0 A'' *)
      ColR.
(* Goal: @TS Tn A' O A0 A'' *)
    apply in_angle_two_sides; Col.
(* Goal: @InAngle Tn A' A0 O A'' *)
    apply lea_in_angle.
(* Goal: @LeA Tn A0 O A' A0 O A'' *)
(* Goal: @OS Tn A0 O A'' A' *)
      apply (l11_30 P Q R P' Q' R'); CongA; apply sams_suma__lea123789 with A0 O A1; trivial.
(* Goal: @OS Tn A0 O A'' A' *)
    apply out_one_side; Col; apply l6_7 with B; [|apply l6_6]; assert_diffs; apply bet_out; auto.
  }
(* Goal: @ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P' Q' R' A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A')))))))) *)
  assert (HConga4 : CongA A O A' A' O A'').
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
  { assert_diffs.
(* Goal: @CongA Tn A O A' A' O A'' *)
    assert (HNOS : ~ OS O A' A0 A'') by (apply l9_9; repeat split; auto; Col; exists A'; Col).
(* Goal: @CongA Tn A O A' A' O A'' *)
    apply conga_trans with A0 O A1; trivial.
(* Goal: @CongA Tn A0 O A1 A' O A'' *)
    apply sams2_suma2__conga456 with P Q R P' Q' R'; trivial.
    - apply (conga2_sams__sams A0 O A' A' O A''); CongA.
(* Goal: @SAMS Tn A0 O A' A' O A'' *)
      split; auto; split.
(* Goal: or (@Out Tn O A' A'') (not (@Bet Tn A0 O A')) *)
(* Goal: @ex (@Tpoint Tn) (fun J : @Tpoint Tn => and (@CongA Tn A' O J A' O A'') (and (not (@OS Tn O A' A0 J)) (and (not (@TS Tn A0 O A' J)) (@Coplanar Tn A0 O A' J)))) *)
        right; intro; Col.
(* Goal: @SumA Tn A0 O A' A' O A'' A0 O A'' *)
      exists A''; repeat (split; CongA); Cop.
(* Goal: not (@TS Tn A0 O A' A'') *)
      apply l9_9_bis, out_one_side; Col.
(* Goal: @Out Tn A0 A' A'' *)
      apply bet_out; auto.
    - apply (conga3_suma__suma A0 O A' A' O A'' A0 O A''); CongA.
(* Goal: @SumA Tn A0 O A' A' O A'' A0 O A'' *)
      exists A''; repeat (split; CongA); Cop.
  }
(* Goal: @ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P' Q' R' A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A')))))))) *)
  assert (HLe'' : Le A0 A1 A' A'').
(* Goal: @Obtuse Tn P Q R *)
    apply le_transitivity with A A'; trivial; assert_diffs.
(* Goal: @Le Tn A A' A' A'' *)
(* Goal: @ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A0 A1 A') (and (@Bet Tn A0 A' B) (and (@CongA Tn P' Q' R' A0 O A') (and (@Le Tn A0 C' A0 A') (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A') (and (@CongA Tn A O A' A0 O A1) (@Le Tn A0 A1 A A')))))))) *)
    apply lt__le, acute_archi_aux with O A0 B; eBetween.
(* Goal: and (@Bet Tn A0 A1 A) (and (@Bet Tn A0 A B) (@CongA Tn P Q R A0 O A)) *)
  exists A''; repeat (split; trivial).
(* Goal: @Le Tn A0 C' A0 A'' *)
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A'') (and (@CongA Tn A O A'' A0 O A1) (@Le Tn A0 A1 A A''))) *)
    apply bet2_le2__le1346 with C A'; auto.
(* Goal: @Le Tn C C' A' A'' *)
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A'') (and (@CongA Tn A O A'' A0 O A1) (@Le Tn A0 A1 A A''))) *)
    apply (l5_6 A0 A1 A' A''); Cong.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => and (@Bet Tn A0 A A'') (and (@CongA Tn A O A'' A0 O A1) (@Le Tn A0 A1 A A''))) *)
  exists A'; split; trivial; split; trivial.
(* Goal: @CongA Tn A' O A'' A0 O A1 *)
  apply conga_trans with A O A'; CongA.
Qed.

Lemma archi_in_acute_angles :
  archimedes_axiom ->
  forall A B C D E F,
    ~ Col A B C -> Acute D E F ->
    exists P Q R, GradA A B C P Q R /\ LeA D E F P Q R.
Proof.
(* Goal: forall (_ : @archimedes_axiom Tn) (A B C D E F : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Acute Tn D E F), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
  intros archi A B C D E F HNCol HAcute.
(* Goal: @Obtuse Tn P Q R *)
  assert_diffs.
(* Goal: not (@TS Tn D E F1 F) *)
  elim (col_dec D E F).
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
  { intro HCol; exists A; exists B; exists C; split.
(* Goal: @GradA Tn A B C A B C *)
(* Goal: @LeA Tn D E F A B C *)
      apply grada_init; CongA.
(* Goal: @LeA Tn D E F A B C *)
    apply l11_31_1; auto; apply not_bet_out; trivial.
(* Goal: not (@Bet Tn D E F) *)
    intro HBet; apply (nlta D E F), acute_obtuse__lta; trivial.
(* Goal: @Obtuse Tn D E F *)
    apply bet__obtuse; auto.
  }
(* Goal: forall _ : not (@Col Tn D E F1), not (@TS Tn D E F1 F) *)
  intro HNCol1.
(* Goal: @LeA Tn A B C D E F *)
(* Goal: @LeA Tn A B C G H I *)
  elim (lea_total D E F A B C); auto; intro HLea.
(* Goal: @GradA Tn A B C A B C *)
(* Goal: @LeA Tn D E F A B C *)
    exists A; exists B; exists C; split; trivial; apply grada_init; CongA.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
  destruct (l8_18_existence D E F) as [D0 [HD0 HD0']]; trivial.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
  assert (HOut : Out E D0 D) by (apply acute_col_perp__out with F; Col; Perp; apply acute_sym; trivial).
(* Goal: @Obtuse Tn P Q R *)
  assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
  assert (HConga : CongA D E F D0 E F) by (apply (out_conga D0 E F D0 E F); CongA; apply out_trivial; auto).
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
  apply (acute_conga__acute D E F D0 E F) in HAcute; trivial.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
  apply (l11_30 A B C D E F A B C D0 E F) in HLea; CongA.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
  apply (ncol_conga_ncol D E F D0 E F) in HNCol1; trivial.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
  assert (HPer : Per E D0 F) by (apply perp_per_1; auto; apply perp_left_comm, perp_col with D; Perp; Col).
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
  clear H0 HD0 HD0' HOut H9.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
  destruct (angle_construction_1 A B C D0 E F) as [D1' [HConga1 HOS]]; trivial.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
  destruct (lea_in_angle D0 E F D1') as [_ [_ [_ [D1 [HBet HUn]]]]]; Side.
(* Goal: @LeA Tn D0 E D1' D0 E F *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
    apply (l11_30 A B C D0 E F); CongA.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
  destruct HUn as [Heq|HOut].
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
    exfalso; subst D1; Col.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
  apply l6_6 in HOut.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
  apply (out_conga A B C D0 E D1' A C D0 D1) in HConga1; trivial; try (apply out_trivial; auto).
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
  apply one_side_not_col123 in HOS.
(* Goal: @Obtuse Tn P Q R *)
  assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
  assert (D0 <> D1) by (intro; subst D1; assert_cols; Col).
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
  clear dependent D1'.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
  destruct (segment_construction D0 F D0 F) as [F' [HF'1 HF'2]].
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
  destruct (archi D0 D1 D0 F') as [G [HG1 HG2]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (@LeA Tn D E F P Q R)))) *)
  destruct (acute_archi_aux2 E D0 D1 F G) as [P [Q [R [HGA HUn]]]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)))))) *)
  exists P; exists Q; exists R; split.
(* Goal: @GradA Tn A B C P Q R *)
(* Goal: @LeA Tn D E F P Q R *)
    assert (Hdistincts := grada_distincts D0 E D1 P Q R HGA); spliter.
(* Goal: @GradA Tn A B C P Q R *)
(* Goal: @LeA Tn D E F P Q R *)
    apply (conga2_grada__grada D0 E D1 P Q R); CongA.
(* Goal: @LeA Tn D E F P Q R *)
  destruct HUn as [HLea2|Habs].
(* Goal: @LeA Tn D E F P Q R *)
(* Goal: @LeA Tn D E F P Q R *)
    assert_diffs; apply (l11_30 D0 E F P Q R); CongA.
(* Goal: @LeA Tn D E F P Q R *)
  exfalso.
(* Goal: False *)
  destruct Habs as [A' [HBet2 [HBet3 [HConga2 [HLe HA]]]]].
(* Goal: False *)
  apply (le__nlt D0 F' D0 G); trivial.
(* Goal: @Lt Tn D0 G D0 F' *)
  apply le1234_lt__lt with D0 F.
(* Goal: @Le Tn D0 G D0 F *)
(* Goal: @Lt Tn D0 F D0 F' *)
    apply le_transitivity with D0 A'; Le.
(* Goal: @Lt Tn D0 F D0 F' *)
  split; Le.
(* Goal: not (@Cong Tn D0 F D0 F') *)
  intro HCong.
(* Goal: False *)
  assert (F = F') by (apply between_cong with D0; trivial).
(* Goal: False *)
  treat_equalities; auto.
Qed.

Lemma angles_archi_aux :
  forall A B C D E F G H I,
    GradA A B C D E F -> GradA A B C G H I -> ~ SAMS D E F G H I ->
    exists P Q R, GradA A B C P Q R /\ ~ SAMS P Q R A B C.
Proof.
(* Goal: forall (A B C D E F G H I : @Tpoint Tn) (_ : @GradA Tn A B C D E F) (_ : @GradA Tn A B C G H I) (_ : not (@SAMS Tn D E F G H I)), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (not (@SAMS Tn P Q R A B C))))) *)
  intros A B C D E F G H I HGA1 HGA2.
(* Goal: forall _ : not (@SAMS Tn D E F G H I), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (not (@SAMS Tn P Q R A B C))))) *)
  induction HGA2.
(* Goal: forall _ : not (@SAMS Tn D E F D0 E0 F0), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (not (@SAMS Tn P Q R A B C))))) *)
(* Goal: forall _ : not (@SAMS Tn D E F G H I), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (not (@SAMS Tn P Q R A B C))))) *)
    intro HNIsi; exists D; exists E; exists F; split; trivial.
(* Goal: not (@SAMS Tn D E F A B C) *)
(* Goal: forall _ : not (@SAMS Tn D E F G H I), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (not (@SAMS Tn P Q R A B C))))) *)
    assert (Hd := grada_distincts A B C D E F HGA1); spliter.
(* Goal: not (@SAMS Tn D E F A B C) *)
(* Goal: forall _ : not (@SAMS Tn D E F G H I), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (not (@SAMS Tn P Q R A B C))))) *)
    intro HIsi; apply HNIsi, (conga2_sams__sams D E F A B C); CongA.
(* Goal: forall _ : not (@SAMS Tn D E F G H I), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (not (@SAMS Tn P Q R A B C))))) *)
  intro HNIsi.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (not (@SAMS Tn P Q R A B C))))) *)
  elim (sams_dec D E F D0 E0 F0); [|apply IHHGA2; trivial].
(* Goal: forall _ : @SAMS Tn D E F D0 E0 F0, @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (not (@SAMS Tn P Q R A B C))))) *)
  intro HIsi; clear IHHGA2.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (not (@SAMS Tn P Q R A B C))))) *)
  assert (Hd := sams_distincts D E F D0 E0 F0 HIsi); spliter.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (not (@SAMS Tn P Q R A B C))))) *)
  destruct (ex_suma D E F D0 E0 F0) as [P [Q [R HSuma]]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)))))) *)
  exists P; exists Q; exists R; split.
(* Goal: @GradA Tn A B C P Q R *)
(* Goal: not (@SAMS Tn P Q R A B C) *)
    apply grada2_sams_suma__grada with D E F D0 E0 F0; trivial.
(* Goal: not (@SAMS Tn P Q R A B C) *)
  intro HIsi2; apply HNIsi, sams_assoc_1 with D0 E0 F0 A B C P Q R; trivial.
Qed.

Lemma angles_archi_aux1 :
  archimedes_axiom ->
  forall A B C D E F,
    ~ Col A B C -> ~ Bet D E F ->
    exists P Q R, GradA A B C P Q R /\ (LeA D E F P Q R \/ ~ SAMS P Q R A B C).
Proof.
(* Goal: forall (_ : @archimedes_axiom Tn) (A B C D E F : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : not (@Bet Tn D E F)), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)))))) *)
  intros archi A B C D E F HNCol HNBet.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)))))) *)
  assert (Hdiff : D <> E /\ F <> E) by (split; intro; subst E; Between); spliter.
(* Goal: @Obtuse Tn P Q R *)
  assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)))))) *)
  destruct (angle_bisector D E F) as [F1 [HInangle HConga]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)))))) *)
  assert(HNOS : ~ OS E F1 D F).
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
  { assert_diffs.
(* Goal: not (@TS Tn D E F1 F) *)
    elim (col_dec D E F1).
(* Goal: forall _ : @Col Tn D E F1, not (@OS Tn E F1 D F) *)
(* Goal: forall _ : not (@Col Tn D E F1), not (@OS Tn E F1 D F) *)
      intros HCol; apply col123__nos; Col.
(* Goal: forall _ : not (@Col Tn D E F1), not (@TS Tn D E F1 F) *)
    intro HNCol1.
(* Goal: not (@OS Tn E F1 D F) *)
    apply l9_9, invert_two_sides, in_angle_two_sides; Col.
(* Goal: not (@Col Tn E F F1) *)
    apply not_col_permutation_1, (ncol_conga_ncol D E F1); CongA.
  }
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)))))) *)
  assert (HSuma : SumA D E F1 D E F1 D E F) by (assert_diffs; exists F; repeat (split; CongA); Cop).
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)))))) *)
  destruct (archi_in_acute_angles archi A B C D E F1) as [P1 [Q1 [R1 [HGA HLea]]]]; trivial.
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
  { apply nbet_sams_suma__acute with D E F; trivial.
(* Goal: @SAMS Tn D E F1 D E F1 *)
    assert_diffs; split; trivial; split.
(* Goal: or (@Out Tn E D F1) (not (@Bet Tn D E F1)) *)
(* Goal: @ex (@Tpoint Tn) (fun J : @Tpoint Tn => and (@CongA Tn F1 E J D E F1) (and (not (@OS Tn E F1 D J)) (and (not (@TS Tn D E F1 J)) (@Coplanar Tn D E F1 J)))) *)
      right; intro HBet; apply HNBet, bet_in_angle_bet with F1; trivial.
(* Goal: @ex (@Tpoint Tn) (fun J : @Tpoint Tn => and (@CongA Tn F1 E J D E F1) (and (not (@OS Tn E F1 D J)) (and (not (@TS Tn D E F1 J)) (@Coplanar Tn D E F1 J)))) *)
    exists F; repeat (split; CongA); Cop.
(* Goal: not (@TS Tn D E F1 F) *)
    elim (col_dec D E F1).
(* Goal: forall _ : @Col Tn D E F1, not (@TS Tn D E F1 F) *)
(* Goal: forall _ : not (@Col Tn D E F1), not (@TS Tn D E F1 F) *)
      intros HCol HTS; destruct HTS; Col.
(* Goal: forall _ : not (@Col Tn D E F1), not (@TS Tn D E F1 F) *)
    intro HNCol1.
(* Goal: not (@TS Tn D E F1 F) *)
    elim (col_dec D E F).
(* Goal: forall _ : @Col Tn D E F, not (@TS Tn D E F1 F) *)
(* Goal: forall _ : not (@Col Tn D E F), not (@TS Tn D E F1 F) *)
      intros HCol HTS; destruct HTS as [_ []]; Col.
(* Goal: forall _ : not (@Col Tn D E F), not (@TS Tn D E F1 F) *)
    intro HNCol2; apply l9_9_bis, in_angle_one_side; Col.
  }
(* Goal: @Obtuse Tn P Q R *)
  assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)))))) *)
  destruct (sams_dec P1 Q1 R1 P1 Q1 R1) as [HIsi|HNIsi].
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
  { destruct (ex_suma P1 Q1 R1 P1 Q1 R1) as [P [Q [R HSuma1]]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)))))) *)
    exists P; exists Q; exists R; split.
(* Goal: @GradA Tn A B C P Q R *)
(* Goal: or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)) *)
      apply grada2_sams_suma__grada with P1 Q1 R1 P1 Q1 R1; trivial.
(* Goal: or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)) *)
    left; apply sams_lea2_suma2__lea with D E F1 D E F1 P1 Q1 R1 P1 Q1 R1; trivial.
  }
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)))))) *)
  destruct (angles_archi_aux A B C P1 Q1 R1 P1 Q1 R1) as [P [Q [R [HGA1 HNsams1]]]]; trivial.
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
  exists P; exists Q; exists R; split; auto.
Qed.

(** Inspired by Hartshorne's demonstration of Lemma 35.1 in Geometry Euclid and Beyond *)
Lemma archi_in_angles :
  archimedes_axiom ->
  forall A B C D E F,
    ~ Col A B C -> D <> E -> F <> E ->
    exists P Q R, GradA A B C P Q R /\ (LeA D E F P Q R \/ ~ SAMS P Q R A B C).
Proof.
(* Goal: forall (_ : @archimedes_axiom Tn) (A B C D E F : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : not (@eq (@Tpoint Tn) D E)) (_ : not (@eq (@Tpoint Tn) F E)), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)))))) *)
  intros archi A B C D E F HNCol HDE HFE.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)))))) *)
  elim (bet_dec D E F); [|apply angles_archi_aux1; trivial].
(* Goal: forall _ : @Bet Tn D E F, @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)))))) *)
  intro HBet1.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (not (@SAMS Tn P Q R A B C))))) *)
  destruct (segment_construction A B A B) as [A0 [HBet HCong]].
(* Goal: @Obtuse Tn P Q R *)
  assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)))))) *)
  assert (HNCol1 : ~ Col A0 B C) by (intro; apply HNCol; ColR).
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)))))) *)
  destruct (angles_archi_aux1 archi A B C C B A0) as [P1 [Q1 [R1 [HGA HUn]]]]; Between.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)))))) *)
  elim (sams_dec P1 Q1 R1 A B C); [|intro; exists P1; exists Q1; exists R1; auto].
(* Goal: not (@SAMS Tn P Q R A B C) *)
  intro HIsi.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)))))) *)
  destruct HUn as [HLea|HNIsi]; [|exfalso; auto].
(* Goal: @Obtuse Tn P Q R *)
  assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)))))) *)
  destruct (ex_suma P1 Q1 R1 A B C) as [P [Q [R HSuma]]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)))))) *)
  exists P; exists Q; exists R; split.
(* Goal: @GradA Tn A B C P Q R *)
(* Goal: or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)) *)
    apply grada_stab with P1 Q1 R1; trivial.
(* Goal: or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)) *)
  suma.assert_diffs.
(* Goal: or (@LeA Tn D E F P Q R) (not (@SAMS Tn P Q R A B C)) *)
  left; apply l11_31_2; auto.
(* Goal: @Bet Tn P Q R *)
  apply (bet_lea__bet A B A0); trivial.
(* Goal: @LeA Tn A B C D E F *)
(* Goal: @LeA Tn A B C G H I *)
  apply sams_lea2_suma2__lea with A0 B C A B C P1 Q1 R1 A B C; Lea.
(* Goal: @SumA Tn A0 B C A B C A B A0 *)
  exists A; repeat (split; CongA); Cop.
(* Goal: @InAngle Tn A1 A0 O B *)
  apply l9_9; repeat split; auto.
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T B C) (@Bet Tn A0 T A)) *)
  exists B; split; Col; Between.
Qed.

(** If Archimedes' postulate holds, every nondegenerate angle can be repeated until exceeding 180° *)
Lemma archi__grada_destruction :
  archimedes_axiom ->
  forall A B C,
    ~ Col A B C ->
    exists P Q R, GradA A B C P Q R /\ ~ SAMS P Q R A B C.
Proof.
(* Goal: forall (_ : @archimedes_axiom Tn) (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradAExp Tn A B C P Q R) (@Obtuse Tn P Q R)))) *)
  intros archi A B C HNCol.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (not (@SAMS Tn P Q R A B C))))) *)
  destruct (segment_construction A B A B) as [A0 [HBet HCong]].
(* Goal: @Obtuse Tn P Q R *)
  assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradA Tn A B C P Q R) (not (@SAMS Tn P Q R A B C))))) *)
  destruct (archi_in_angles archi A B C A B A0) as [P [Q [R [HGA HUn]]]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
  exists P; exists Q; exists R; split; auto.
(* Goal: not (@SAMS Tn P Q R A B C) *)
  destruct HUn as [HLea|]; trivial.
(* Goal: not (@SAMS Tn P Q R A B C) *)
  intro HIsi.
(* Goal: False *)
  destruct HIsi as [_ [[HOut|HNBet] _]].
(* Goal: False *)
(* Goal: False *)
    apply HNCol; Col.
(* Goal: False *)
  apply HNBet, (bet_lea__bet A B A0); trivial.
Qed.


Lemma gradaexp_destruction_aux : forall A B C P Q R,
  GradA A B C P Q R ->
  exists S T U, GradAExp A B C S T U /\ (Obtuse S T U \/ LeA P Q R S T U).
Proof.
(* Goal: forall (A B C P Q R : @Tpoint Tn) (_ : @GradA Tn A B C P Q R), @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn P Q R S T U))))) *)
  intros A B C.
(* Goal: forall (P Q R : @Tpoint Tn) (_ : @GradA Tn A B C P Q R), @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn P Q R S T U))))) *)
  induction 1.
(* Goal: @LeA Tn A B C D E F *)
(* Goal: @LeA Tn A B C G H I *)
    assert_diffs; exists D; exists E; exists F; split; [apply gradaexp_init|right]; Lea.
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
  destruct IHGradA as [P [Q [R [HGAE HUn]]]].
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
  assert (Hd := HGAE); apply gradaexp__grada, grada_distincts in Hd; spliter.
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
  destruct (sams_dec P Q R P Q R) as [HIsi|HNIsi].
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
  { destruct HUn as [Habs|HLea].
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
      absurd (SAMS P Q R P Q R); trivial; apply obtuse__nsams, Habs.
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
    destruct (ex_suma P Q R P Q R) as [S [T [U HSuma]]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
    exists S; exists T; exists U; split.
(* Goal: @GradAExp Tn A B C S T U *)
(* Goal: or (@Obtuse Tn S T U) (@LeA Tn G H I S T U) *)
      apply gradaexp_stab with P Q R; trivial.
(* Goal: or (@Obtuse Tn S T U) (@LeA Tn G H I S T U) *)
    right; apply sams_lea2_suma2__lea with D E F A B C P Q R P Q R; trivial.
(* Goal: @LeA Tn A B C P Q R *)
    apply grada__lea, gradaexp__grada, HGAE.
  }
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
  apply nsams__obtuse in HNIsi; auto.
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => @ex (@Tpoint Tn) (fun U : @Tpoint Tn => and (@GradAExp Tn A B C S T U) (or (@Obtuse Tn S T U) (@LeA Tn G H I S T U))))) *)
  exists P; exists Q; exists R; split; auto.
Qed.

(** If Archimedes' postulate holds, every nondegenerate angle can be doubled until exceeding 90° *)
Lemma archi__gradaexp_destruction :
  archimedes_axiom ->
  forall A B C,
    ~ Col A B C ->
    exists P Q R, GradAExp A B C P Q R /\ Obtuse P Q R.
Proof.
(* Goal: forall (_ : @archimedes_axiom Tn) (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradAExp Tn A B C P Q R) (@Obtuse Tn P Q R)))) *)
  intros archi A B C HNCol.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradAExp Tn A B C P Q R) (@Obtuse Tn P Q R)))) *)
  destruct (archi__grada_destruction archi A B C HNCol) as [D [E [F [HGA HNIsi]]]].
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradAExp Tn A B C P Q R) (@Obtuse Tn P Q R)))) *)
  destruct (gradaexp_destruction_aux A B C D E F HGA) as [P [Q [R [HGAE HUn]]]].
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@GradAExp Tn A B C P Q R) (@Obtuse Tn P Q R)))) *)
  exists P; exists Q; exists R; split; trivial.
(* Goal: @Obtuse Tn P Q R *)
  destruct HUn as [HObtuse|HLea]; trivial.
(* Goal: @Obtuse Tn P Q R *)
  assert_diffs.
(* Goal: @Obtuse Tn P Q R *)
  apply nsams__obtuse; auto.
(* Goal: not (@SAMS Tn P Q R P Q R) *)
  intro HIsi; apply HNIsi.
(* Goal: @SAMS Tn D E F A B C *)
  apply sams_lea2__sams with P Q R P Q R; trivial.
(* Goal: @LeA Tn A B C P Q R *)
  apply grada__lea, gradaexp__grada, HGAE.
Qed.

End Archimedes_for_angles.