Require Import GeoCoq.Axioms.continuity_axioms.
Require Import GeoCoq.Axioms.parallel_postulates.
Require Export GeoCoq.Meta_theory.Parallel_postulates.SPP_ID.
Require Export GeoCoq.Meta_theory.Parallel_postulates.TCP_tarski.
Require Export GeoCoq.Meta_theory.Parallel_postulates.alternate_interior_angles_proclus.
Require Export GeoCoq.Meta_theory.Continuity.angle_archimedes.
Require Export GeoCoq.Meta_theory.Continuity.archimedes.
Require Export GeoCoq.Meta_theory.Continuity.aristotle.
Require Export GeoCoq.Meta_theory.Parallel_postulates.euclid_5_original_euclid.
Require Export GeoCoq.Meta_theory.Parallel_postulates.existential_triangle_rah.
Require Export GeoCoq.Meta_theory.Parallel_postulates.par_perp_perp_TCP.
Require Export GeoCoq.Meta_theory.Parallel_postulates.playfair_alternate_interior_angles.
Require Export GeoCoq.Meta_theory.Parallel_postulates.playfair_bis_playfair.
Require Export GeoCoq.Meta_theory.Parallel_postulates.playfair_universal_posidonius_postulate.
Require Export GeoCoq.Meta_theory.Parallel_postulates.proclus_SPP.
Require Export GeoCoq.Meta_theory.Parallel_postulates.rah_triangle.
Require Export GeoCoq.Meta_theory.Parallel_postulates.tarski_euclid.
Require Export GeoCoq.Meta_theory.Parallel_postulates.triangle_playfair_bis.
Require Export GeoCoq.Meta_theory.Parallel_postulates.triangle_existential_triangle.
Require Export GeoCoq.Meta_theory.Parallel_postulates.universal_posidonius_postulate_par_perp_perp.
Require Export GeoCoq.Tarski_dev.Annexes.defect.

Section Legendre.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Theorem stronger_legendre_s_first_theorem :
  aristotle_s_axiom ->
  forall A B C D E F,
    SumA C A B A B C D E F ->
    SAMS D E F B C A.
Proof.
(* Goal: forall (_ : @aristotle_s_axiom Tn) (A B C D E F : @Tpoint Tn) (_ : @SumA Tn C A B A B C D E F), @SAMS Tn D E F B C A *)
  intros ari A B C D E F.
(* Goal: forall _ : @SumA Tn C A B A B C D E F, @SAMS Tn D E F B C A *)
  apply (t22_20 (aristotle__obtuse_case_elimination ari)).
Qed.

Theorem legendre_s_first_theorem :
  archimedes_axiom ->
  forall A B C D E F,
    SumA C A B A B C D E F ->
    SAMS D E F B C A.
Proof.
(* Goal: forall (_ : @archimedes_axiom Tn) (A B C D E F : @Tpoint Tn) (_ : @SumA Tn C A B A B C D E F), @SAMS Tn D E F B C A *)
  intros archi A B C D E F.
(* Goal: forall _ : @SumA Tn C A B A B C D E F, @SAMS Tn D E F B C A *)
  apply (t22_20 (archi__obtuse_case_elimination archi)).
Qed.

Theorem legendre_s_second_theorem :
  postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights ->
  triangle_postulate.
Proof.
(* Goal: forall _ : @postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn, @triangle_postulate Tn *)
  assert (H:=existential_triangle__rah); assert (I:=rah__triangle); tauto.
Qed.

Lemma legendre_s_third_theorem_aux :
  aristotle_s_axiom ->
  triangle_postulate ->
  euclid_s_parallel_postulate.
Proof.
(* Goal: forall (_ : @aristotle_s_axiom Tn) (_ : @triangle_postulate Tn), @euclid_s_parallel_postulate Tn *)
  assert (I:=aristotle__greenberg).
(* Goal: forall (_ : @aristotle_s_axiom Tn) (_ : @triangle_postulate Tn), @euclid_s_parallel_postulate Tn *)
  assert (J:playfair_s_postulate->greenberg_s_axiom->decidability_of_intersection).
(* Goal: @TS Tn C B1 B D *)
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  { intro HP; assert (J:=playfair__alternate_interior HP).
(* Goal: forall _ : @greenberg_s_axiom Tn, @decidability_of_intersection Tn *)
    assert(K:=alternate_interior__proclus).
(* Goal: forall _ : @greenberg_s_axiom Tn, @decidability_of_intersection Tn *)
    assert(L:proclus_postulate->decidability_of_intersection); [|tauto].
(* Goal: forall _ : @proclus_postulate Tn, @decidability_of_intersection Tn *)
    assert(M:=proclus_s_postulate_implies_strong_parallel_postulate).
(* Goal: forall _ : @proclus_postulate Tn, @decidability_of_intersection Tn *)
    assert(N:=strong_parallel_postulate_implies_inter_dec); tauto.
  }
(* Goal: forall (_ : @aristotle_s_axiom Tn) (_ : @triangle_postulate Tn), @euclid_s_parallel_postulate Tn *)
  assert (K:=triangle__playfair_bis).
(* Goal: forall (_ : @aristotle_s_axiom Tn) (_ : @triangle_postulate Tn), @euclid_s_parallel_postulate Tn *)
  assert (L:=playfair_bis__playfair).
(* Goal: forall (_ : @aristotle_s_axiom Tn) (_ : @triangle_postulate Tn), @euclid_s_parallel_postulate Tn *)
  assert (M:=playfair__universal_posidonius_postulate).
(* Goal: forall (_ : @aristotle_s_axiom Tn) (_ : @triangle_postulate Tn), @euclid_s_parallel_postulate Tn *)
  assert (N:=universal_posidonius_postulate__perpendicular_transversal_postulate).
(* Goal: forall (_ : @aristotle_s_axiom Tn) (_ : @triangle_postulate Tn), @euclid_s_parallel_postulate Tn *)
  assert (O:=inter_dec_plus_par_perp_perp_imply_triangle_circumscription).
(* Goal: forall (_ : @aristotle_s_axiom Tn) (_ : @triangle_postulate Tn), @euclid_s_parallel_postulate Tn *)
  assert (P:=triangle_circumscription_implies_tarski_s_euclid).
(* Goal: forall (_ : @aristotle_s_axiom Tn) (_ : @triangle_postulate Tn), @euclid_s_parallel_postulate Tn *)
  assert (Q:=tarski_s_euclid_implies_euclid_5).
(* Goal: forall (_ : @aristotle_s_axiom Tn) (_ : @triangle_postulate Tn), @euclid_s_parallel_postulate Tn *)
  assert (R:=euclid_5__original_euclid); tauto.
Qed.

Theorem legendre_s_third_theorem :
  archimedes_axiom ->
  triangle_postulate ->
  euclid_s_parallel_postulate.
Proof.
(* Goal: forall (_ : @archimedes_axiom Tn) (_ : @triangle_postulate Tn), @euclid_s_parallel_postulate Tn *)
  assert (H:=t22_24); assert (I:=legendre_s_third_theorem_aux); tauto.
Qed.

Lemma legendre_aux :
  ~ hypothesis_of_obtuse_saccheri_quadrilaterals ->
  forall A B C D B1 C1 P Q R S T U V W X,
    ~ Col A B C -> CongA A C B C B D ->
    Cong A C B D -> TS B C A D -> Out A B B1 -> Out A C C1 -> Bet B1 D C1 ->
    Defect A B C P Q R -> Defect A B1 C1 S T U -> SumA P Q R P Q R V W X ->
    SAMS P Q R P Q R /\ LeA V W X S T U.
Proof.
(* Goal: forall (_ : not (@hypothesis_of_obtuse_saccheri_quadrilaterals Tn)) (A B C D B1 C1 P Q R S T U V W X : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @CongA Tn A C B C B D) (_ : @Cong Tn A C B D) (_ : @TS Tn B C A D) (_ : @Out Tn A B B1) (_ : @Out Tn A C C1) (_ : @Bet Tn B1 D C1) (_ : @Defect Tn A B C P Q R) (_ : @Defect Tn A B1 C1 S T U) (_ : @SumA Tn P Q R P Q R V W X), and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  intros noah A B C D B1 C1 P Q R S T U V W X HNCol HConga HCong HTS HOutB HOutC HBet HDef HDef1 HSuma.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  destruct (l11_49 A C B D B C) as [HCong1 [HConga1 HConga2]]; CongA; Cong.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
    assert_diffs; auto.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  assert (HPar : Par_strict A C B D).
(* Goal: @TS Tn C B1 B D *)
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  { apply par_not_col_strict with B; Col.
(* Goal: @Par Tn A B C D *)
    apply par_left_comm, l12_21_b; Side; CongA.
  }
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  assert (HPar' : Par_strict A B C D).
(* Goal: @TS Tn C B1 B D *)
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  { apply par_not_col_strict with C; Col.
(* Goal: @Par Tn A B C D *)
    apply par_left_comm, l12_21_b; Side; CongA.
  }
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  assert (HNCol2:= HPar'); assert (HNCol3 := HPar'); assert (HNCol4 := HPar').
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  apply par_strict_not_col_2 in HNCol2; apply par_strict_not_col_3 in HNCol3; apply par_strict_not_col_4 in HNCol4.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  assert (HB : ~ Col B1 B D /\ TS B D B1 C1 /\ Bet A B B1).
(* Goal: @TS Tn C B1 B D *)
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  { assert_diffs.
(* Goal: and (not (@Col Tn B1 B D)) (and (@TS Tn B D B1 C1) (@Bet Tn A B B1)) *)
    apply par_strict_symmetry, (par_strict_col_par_strict B D A C C1) in HPar; Col.
(* Goal: and (not (@Col Tn B1 B D)) (and (@TS Tn B D B1 C1) (@Bet Tn A B B1)) *)
    assert (HNCol' := par_strict_not_col_4 B D A C1 HPar).
(* Goal: and (not (@Col Tn B1 B D)) (and (@TS Tn B D B1 C1) (@Bet Tn A B B1)) *)
    assert (B <> B1) by (intro; subst B1; apply HNCol'; Col).
(* Goal: and (not (@Col Tn B1 B D)) (and (@TS Tn B D B1 C1) (@Bet Tn A B B1)) *)
    assert (~ Col B1 B D) by (intro; apply HNCol4; ColR).
(* Goal: and (not (@Col Tn B1 B D)) (and (@TS Tn B D B1 C1) (@Bet Tn A B B1)) *)
    assert (TS B D B1 C1) by (repeat split; Col; exists D; Col).
(* Goal: and (not (@Col Tn B1 B D)) (and (@TS Tn B D B1 C1) (@Bet Tn A B B1)) *)
    repeat (split; auto).
(* Goal: @Bet Tn A C C1 *)
    apply col_two_sides_bet with D; Col.
(* Goal: @TS Tn B D A B1 *)
    apply l9_8_2 with C1; Side.
  }
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  destruct HB as [HNCol5 [HTS1 HBetB]].
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  assert (HC : ~ Col C D B1 /\ C <> C1 /\ Bet A C C1).
(* Goal: @TS Tn C B1 B D *)
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  { assert_diffs.
(* Goal: and (not (@Col Tn C D B1)) (and (not (@eq (@Tpoint Tn) C C1)) (@Bet Tn A C C1)) *)
    apply par_strict_symmetry, (par_strict_col_par_strict C D A B B1) in HPar'; Col.
(* Goal: and (not (@Col Tn C D B1)) (and (not (@eq (@Tpoint Tn) C C1)) (@Bet Tn A C C1)) *)
    assert (HNCol' := par_strict_not_col_4 C D A B1 HPar').
(* Goal: and (not (@Col Tn C D B1)) (and (not (@eq (@Tpoint Tn) C C1)) (@Bet Tn A C C1)) *)
    assert (C <> C1) by (intro; subst C1; apply HNCol'; Col).
(* Goal: @InAngle Tn D' B' A C' *)
(* Goal: and (@CongA Tn A C' B' C' B' D') (and (@Cong Tn A C' B' D') (@TS Tn B' C' A D')) *)
    repeat split; auto.
(* Goal: @Bet Tn A C C1 *)
    apply col_two_sides_bet with D; Col.
(* Goal: @TS Tn C D A C1 *)
    apply l9_8_2 with B1; Side.
(* Goal: @TS Tn B' C' A D' *)
    repeat split; Col.
(* Goal: not (@Col Tn C1 C D) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T C D) (@Bet Tn B1 T C1)) *)
      intro; apply HNCol3; ColR.
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T C D) (@Bet Tn B1 T C1)) *)
    exists D; Col.
  }
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  destruct HC as [HNCol6 [HCC1 HBetC]].
(* Goal: @SAMS Tn P' Q' R' P' Q' R' *)
  assert_diffs.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  destruct (ts2__ex_bet2 B C D B1) as [Z [HZ1 HZ2]].
(* Goal: @TS Tn B D C B1 *)
(* Goal: @TS Tn C B1 B D *)
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
    apply l9_8_2 with C1; Side; apply one_side_symmetry, l12_6, par_strict_col_par_strict with A; Col; Par.
(* Goal: @TS Tn C B1 B D *)
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
    { apply l9_31.
(* Goal: @OS Tn C B B1 D *)
(* Goal: @OS Tn C D B1 B *)
        apply l9_17 with C1; trivial.
        exists A; assert_diffs; repeat split; Col; try (intro; apply HNCol; ColR);
        [exists B|exists C]; split; Col; Between.
(* Goal: @OS Tn C D B1 B *)
      apply one_side_symmetry, l12_6, par_strict_col_par_strict with A; Col; Par.
    }

(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  rename H into HAB1.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  destruct (ex_defect A B1 C) as [G [H [I HDef2]]]; auto.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  destruct (ex_defect B1 C C1) as [J [K [L HDef3]]]; auto.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  destruct (ex_defect C B B1) as [M [N [O HDef4]]]; auto.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  destruct (ex_defect B1 C D) as [A' [B' [C' HDef5]]]; auto.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  destruct (ex_defect C D C1) as [D' [E' [F' HDef6]]]; auto.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  destruct (ex_defect B1 B D) as [M' [N' [O' HDef7]]]; auto.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  assert (Hd := defect_distincts A B1 C G H I HDef2).
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  assert (Hd2 := defect_distincts C B B1 M N O HDef4).
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  assert (Hd3 := defect_distincts B1 C D A' B' C' HDef5).
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  spliter; clean.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  destruct (ex_suma G H I A' B' C') as [G' [H' [I' HSuma1]]]; auto.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  destruct (ex_suma M N O A' B' C') as [J' [K' [L' HSuma2]]]; auto.

(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  destruct (t22_16_1bis noah A B1 C1 C G H I J K L S T U) as [HIsi3 HSuma3]; trivial.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  destruct (t22_16_1bis noah B1 C C1 D A' B' C' D' E' F' J K L) as [HIsi4 HSuma4]; trivial.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  destruct (t22_16_1bis noah A C B1 B P Q R M N O G H I) as [HIsi5 HSuma5]; trivial.
(* Goal: @Defect Tn A C B P Q R *)
(* Goal: @Defect Tn A C B1 G H I *)
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
    apply defect_perm_132, HDef.
(* Goal: @Defect Tn A C B1 G H I *)
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
    apply defect_perm_132, HDef2.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  assert (HIsi1 : SAMS G H I A' B' C').
(* Goal: @SAMS Tn G H I A' B' C' *)
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
    apply sams_lea2__sams with G H I J K L; Lea.
(* Goal: @LeA Tn G' H' I' S T U *)
    apply sams_suma__lea123789 with D' E' F'; trivial.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  assert (HIsi2 : SAMS M N O A' B' C').
(* Goal: @SAMS Tn M N O A' B' C' *)
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
    apply sams_lea2__sams with G H I A' B' C'; Lea.
(* Goal: @LeA Tn M N O G H I *)
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
    apply sams_suma__lea456789 with P Q R; trivial.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  assert (HSuma6 : SumA G' H' I' D' E' F' S T U).
(* Goal: @SumA Tn G' H' I' D' E' F' S T U *)
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
    apply suma_assoc_2 with G H I A' B' C' J K L; trivial.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  assert (HIsi6 : SAMS G' H' I' D' E' F').
(* Goal: @SAMS Tn G' H' I' D' E' F' *)
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
    apply sams_assoc_2 with G H I A' B' C' J K L; trivial.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  assert (HSuma7 : SumA P Q R J' K' L' G' H' I').
(* Goal: @SumA Tn P Q R J' K' L' G' H' I' *)
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
    apply suma_assoc_1 with M N O A' B' C' G H I; trivial.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  assert (HIsi7 : SAMS P Q R J' K' L').
(* Goal: @SAMS Tn P Q R J' K' L' *)
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
    apply sams_assoc_1 with M N O A' B' C' G H I; trivial.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  destruct (t22_16_2 noah C B B1 D M' N' O' A' B' C' P Q R M N O Z J' K' L') as [HIsi8 HSuma8]; trivial.
(* Goal: @Defect Tn C B D P Q R *)
(* Goal: @Defect Tn C D B1 A' B' C' *)
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
    apply defect_perm_231, (conga3_defect__defect A B C); CongA.
(* Goal: @Defect Tn C D B1 A' B' C' *)
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
    apply defect_perm_231, HDef5.
(* Goal: and (@SAMS Tn P Q R P Q R) (@LeA Tn V W X S T U) *)
  assert (HLea : LeA P Q R J' K' L') by (apply sams_suma__lea123789 with M' N' O'; trivial).

(* Goal: and (@CongA Tn A C' B' C' B' D') (and (@Cong Tn A C' B' D') (@TS Tn B' C' A D')) *)
  split.
(* Goal: @SAMS Tn P' Q' R' P' Q' R' *)
    suma.assert_diffs.
(* Goal: @SAMS Tn P Q R P Q R *)
(* Goal: @LeA Tn V W X S T U *)
    apply sams_lea2__sams with P Q R J' K' L'; Lea.
(* Goal: @LeA Tn V W X S T U *)
  apply lea_trans with G' H' I'.
(* Goal: @LeA Tn V W X G' H' I' *)
(* Goal: @LeA Tn G' H' I' S T U *)
    apply sams_lea456_suma2__lea with P Q R P Q R J' K' L'; trivial.
(* Goal: @LeA Tn G' H' I' S T U *)
  apply sams_suma__lea123789 with D' E' F'; trivial.
Qed.

Lemma legendre_aux1 : forall A B C B' C',
  ~ Col A B C -> Out A B B' -> Out A C C' ->
  exists D', InAngle D' B A C /\ CongA A C' B' C' B' D' /\
             Cong A C' B' D' /\ TS B' C' A D'.
Proof.
(* Goal: forall (A B C B' C' : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Out Tn A B B') (_ : @Out Tn A C C'), @ex (@Tpoint Tn) (fun D' : @Tpoint Tn => and (@InAngle Tn D' B A C) (and (@CongA Tn A C' B' C' B' D') (and (@Cong Tn A C' B' D') (@TS Tn B' C' A D')))) *)
  intros A B C B' C' HNCol HOutB HOutC.
(* Goal: @SAMS Tn P' Q' R' P' Q' R' *)
  assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun D' : @Tpoint Tn => and (@InAngle Tn D' B A C) (and (@CongA Tn A C' B' C' B' D') (and (@Cong Tn A C' B' D') (@TS Tn B' C' A D')))) *)
  assert (HNCol' : ~ Col A B' C') by (intro; assert_diffs; apply HNCol; ColR).
(* Goal: @ex (@Tpoint Tn) (fun D' : @Tpoint Tn => and (@InAngle Tn D' B A C) (and (@CongA Tn A C' B' C' B' D') (and (@Cong Tn A C' B' D') (@TS Tn B' C' A D')))) *)
  destruct (midpoint_existence B' C') as [M HM].
(* Goal: @ex (@Tpoint Tn) (fun D' : @Tpoint Tn => and (@InAngle Tn D' B A C) (and (@CongA Tn A C' B' C' B' D') (and (@Cong Tn A C' B' D') (@TS Tn B' C' A D')))) *)
  destruct (symmetric_point_construction A M) as [D' HD].
(* Goal: @ex (@Tpoint Tn) (fun D' : @Tpoint Tn => and (@InAngle Tn D' B A C) (and (@CongA Tn A C' B' C' B' D') (and (@Cong Tn A C' B' D') (@TS Tn B' C' A D')))) *)
  assert (HNCol1 : ~ Col A M B') by (intro; assert_diffs; apply HNCol'; ColR).
(* Goal: @ex (@Tpoint Tn) (fun D' : @Tpoint Tn => and (@InAngle Tn D' B A C) (and (@CongA Tn A C' B' C' B' D') (and (@Cong Tn A C' B' D') (@TS Tn B' C' A D')))) *)
  assert (HNCol2 : ~ Col D' B' C') by (intro; assert_diffs; apply HNCol'; ColR).
(* Goal: @ex (@Tpoint Tn) (fun D' : @Tpoint Tn => and (@InAngle Tn D' B A C) (and (@CongA Tn A C' B' C' B' D') (and (@Cong Tn A C' B' D') (@TS Tn B' C' A D')))) *)
  exists D'.
(* Goal: and (@CongA Tn A C' B' C' B' D') (and (@Cong Tn A C' B' D') (@TS Tn B' C' A D')) *)
  assert_diffs; destruct HM; destruct HD; split.
(* Goal: @InAngle Tn D' B A C *)
(* Goal: and (@CongA Tn A C' B' C' B' D') (and (@Cong Tn A C' B' D') (@TS Tn B' C' A D')) *)
    apply l11_25 with D' B' C'; try (apply out_trivial); auto.
(* Goal: @InAngle Tn D' B' A C' *)
(* Goal: and (@CongA Tn A C' B' C' B' D') (and (@Cong Tn A C' B' D') (@TS Tn B' C' A D')) *)
    repeat split; auto.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn B' X C') (or (@eq (@Tpoint Tn) X A) (@Out Tn A X D'))) *)
(* Goal: and (@CongA Tn A C' B' C' B' D') (and (@Cong Tn A C' B' D') (@TS Tn B' C' A D')) *)
    exists M; split; trivial.
(* Goal: or (@eq (@Tpoint Tn) M A) (@Out Tn A M D') *)
(* Goal: and (@CongA Tn A C' B' C' B' D') (and (@Cong Tn A C' B' D') (@TS Tn B' C' A D')) *)
    right; apply bet_out; auto.
(* Goal: and (@CongA Tn A C' B' C' B' D') (and (@Cong Tn A C' B' D') (@TS Tn B' C' A D')) *)
  destruct (l11_49 A M C' D' M B') as [HCong1 [HConga1 HConga2]]; Cong.
(* Goal: @CongA Tn A M C' D' M B' *)
(* Goal: and (@CongA Tn A C' B' C' B' D') (and (@Cong Tn A C' B' D') (@TS Tn B' C' A D')) *)
    apply l11_14; Between.
(* Goal: and (@CongA Tn A C' B' C' B' D') (and (@Cong Tn A C' B' D') (@TS Tn B' C' A D')) *)
  split.
(* Goal: @CongA Tn A C' B' C' B' D' *)
(* Goal: and (@Cong Tn A C' B' D') (@TS Tn B' C' A D') *)
    apply (out_conga A C' M M B' D'); try (apply out_trivial); try (apply bet_out); Between; CongA.
(* Goal: and (@Cong Tn A C' B' D') (@TS Tn B' C' A D') *)
  split; Cong.
(* Goal: @TS Tn B' C' A D' *)
  repeat split; Col.
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T B' C') (@Bet Tn A T D')) *)
  exists M; split; Col.
Qed.

Lemma legendre_aux2 :
  ~ hypothesis_of_obtuse_saccheri_quadrilaterals ->
  forall A B C,
    ~ Col A B C ->  Acute B A C ->
    (forall T,
       InAngle T B A C ->
       exists X Y : Tpoint, Out A B X /\ Out A C Y /\ Bet X T Y) ->
    forall P Q R S T U,
      Defect A B C P Q R -> GradAExp P Q R S T U ->
      exists B' C' P' Q' R',
        (Out A B B' /\ Out A C C' /\
         Defect A B' C' P' Q' R' /\ LeA S T U P' Q' R').
Proof.
(* Goal: forall (_ : not (@hypothesis_of_obtuse_saccheri_quadrilaterals Tn)) (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Acute Tn B A C) (_ : forall (T : @Tpoint Tn) (_ : @InAngle Tn T B A C), @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn A B X) (and (@Out Tn A C Y) (@Bet Tn X T Y))))) (P Q R S T U : @Tpoint Tn) (_ : @Defect Tn A B C P Q R) (_ : @GradAExp Tn P Q R S T U), @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @ex (@Tpoint Tn) (fun P' : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q' : @Tpoint Tn => @ex (@Tpoint Tn) (fun R' : @Tpoint Tn => and (@Out Tn A B B') (and (@Out Tn A C C') (and (@Defect Tn A B' C' P' Q' R') (@LeA Tn S T U P' Q' R')))))))) *)
  intros noah A B C HNCol HAcute legendre P Q R S T U HDef.
(* Goal: forall _ : @GradAExp Tn P Q R S T U, @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @ex (@Tpoint Tn) (fun P' : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q' : @Tpoint Tn => @ex (@Tpoint Tn) (fun R' : @Tpoint Tn => and (@Out Tn A B B') (and (@Out Tn A C C') (and (@Defect Tn A B' C' P' Q' R') (@LeA Tn S T U P' Q' R')))))))) *)
  induction 1; rename A0 into P; rename B0 into Q; rename C0 into R.
(* Goal: @SAMS Tn P' Q' R' P' Q' R' *)
    exists B; exists C; exists P; exists Q; exists R; assert_diffs.
(* Goal: and (@Out Tn A B B) (and (@Out Tn A C C) (and (@Defect Tn A B C P Q R) (@LeA Tn D E F P Q R))) *)
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @ex (@Tpoint Tn) (fun P' : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q' : @Tpoint Tn => @ex (@Tpoint Tn) (fun R' : @Tpoint Tn => and (@Out Tn A B B') (and (@Out Tn A C C') (and (@Defect Tn A B' C' P' Q' R') (@LeA Tn G H I P' Q' R')))))))) *)
    repeat split; (try apply out_trivial); Lea.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @ex (@Tpoint Tn) (fun P' : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q' : @Tpoint Tn => @ex (@Tpoint Tn) (fun R' : @Tpoint Tn => and (@Out Tn A B B') (and (@Out Tn A C C') (and (@Defect Tn A B' C' P' Q' R') (@LeA Tn G H I P' Q' R')))))))) *)
  rename D into S; rename E into T; rename F into U.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @ex (@Tpoint Tn) (fun P' : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q' : @Tpoint Tn => @ex (@Tpoint Tn) (fun R' : @Tpoint Tn => and (@Out Tn A B B') (and (@Out Tn A C C') (and (@Defect Tn A B' C' P' Q' R') (@LeA Tn G H I P' Q' R')))))))) *)
  destruct IHGradAExp as [B' [C' [P' [Q' [R' [HOutB [HOutC [HDef' HLea]]]]]]]]; trivial.
(* Goal: @SAMS Tn P' Q' R' P' Q' R' *)
  destruct (legendre_aux1 A B C B' C') as [D' [HInangle [HConga [HCong HTS]]]]; trivial.
(* Goal: @SAMS Tn P' Q' R' P' Q' R' *)
  assert (HNCol' : ~ Col A B' C') by (destruct HTS; Col).
(* Goal: @SAMS Tn P' Q' R' P' Q' R' *)
  destruct (legendre D' HInangle) as [B'' [C'' [HOutB' [HOutC' HBet]]]].
(* Goal: @SAMS Tn P' Q' R' P' Q' R' *)
  assert (Hd := defect_distincts A B' C' P' Q' R' HDef'); spliter; assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @ex (@Tpoint Tn) (fun P' : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q' : @Tpoint Tn => @ex (@Tpoint Tn) (fun R' : @Tpoint Tn => and (@Out Tn A B B') (and (@Out Tn A C C') (and (@Defect Tn A B' C' P' Q' R') (@LeA Tn G H I P' Q' R')))))))) *)
  destruct (ex_defect A B'' C'') as [P'' [Q'' [R'' HDef'']]]; auto.
(* Goal: not (@eq (@Tpoint Tn) B'' C'') *)
(* Goal: @SAMS Tn P' Q' R' P' Q' R' *)
    intro; subst; apply HNCol; ColR.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @ex (@Tpoint Tn) (fun P' : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q' : @Tpoint Tn => @ex (@Tpoint Tn) (fun R' : @Tpoint Tn => and (@Out Tn A B B') (and (@Out Tn A C C') (and (@Defect Tn A B' C' P' Q' R') (@LeA Tn G H I P' Q' R')))))))) *)
  exists B''; exists C''; exists P''; exists Q''; exists R''.
(* Goal: and (@Out Tn A B B'') (and (@Out Tn A C C'') (and (@Defect Tn A B'' C'' P'' Q'' R'') (@LeA Tn G H I P'' Q'' R''))) *)
  repeat (split; trivial).
(* Goal: @LeA Tn G H I P'' Q'' R'' *)
  destruct (ex_suma P' Q' R' P' Q' R') as [V [W [X HSuma1]]]; auto.
(* Goal: @LeA Tn G H I P'' Q'' R'' *)
  destruct (legendre_aux noah A B' C' D' B'' C'' P' Q' R' P'' Q'' R'' V W X) as [HIsi1 HLea1]; trivial.
(* Goal: @Out Tn A B' B'' *)
(* Goal: @Out Tn A C' C'' *)
(* Goal: @LeA Tn G H I P'' Q'' R'' *)
    apply l6_7 with B; trivial; apply l6_6; trivial.
(* Goal: @Out Tn A C' C'' *)
(* Goal: @LeA Tn G H I P'' Q'' R'' *)
    apply l6_7 with C; trivial; apply l6_6; trivial.
(* Goal: @LeA Tn G H I P'' Q'' R'' *)
  apply lea_trans with V W X; trivial.
(* Goal: @LeA Tn G H I V W X *)
  apply sams_lea2_suma2__lea with S T U S T U P' Q' R' P' Q' R'; trivial.
Qed.

Lemma legendre_s_fourth_theorem_aux :
  archimedes_axiom ->
  legendre_s_parallel_postulate ->
  postulate_of_right_saccheri_quadrilaterals.
Proof.
(* Goal: forall (_ : @archimedes_axiom Tn) (_ : @legendre_s_parallel_postulate Tn), @postulate_of_right_saccheri_quadrilaterals Tn *)
  intros archi legendre.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  destruct legendre as [B [A [C [HNCol [HAcute legendre]]]]].
(* Goal: @SAMS Tn P' Q' R' P' Q' R' *)
  assert_diffs.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  destruct (ex_defect A B C) as [P [Q [R HDef]]]; auto.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  destruct (col_dec P Q R) as [HCol|HNCol1].
  - apply archi__obtuse_case_elimination in archi.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
    apply (defect_ncol_out__rah A B C P Q R); Col.
(* Goal: @Out Tn Q P R *)
    apply not_bet_out; Col.
(* Goal: not (@Bet Tn P Q R) *)
    intro HBet.
(* Goal: False *)
    apply HNCol.
(* Goal: @Col Tn B A C *)
    apply defect_perm_213 in HDef.
(* Goal: @Col Tn B A C *)
    destruct HDef as [D [E [F [[G [H [I [HSuma1 HSuma2]]]] HSuppa]]]].
(* Goal: @Col Tn B A C *)
    apply out_col, l6_6, out_lea__out with D E F.
(* Goal: @Out Tn E D F *)
(* Goal: @LeA Tn C B A D E F *)
      apply (bet_suppa__out P Q R); [|apply suppa_sym]; assumption.
(* Goal: @LeA Tn C B A D E F *)
    apply sams_suma__lea456789 with G H I; trivial.
(* Goal: @SAMS Tn G H I C B A *)
    apply (t22_20 archi); trivial.
  - destruct (archi__gradaexp_destruction archi P Q R HNCol1) as [S [T [U [HGAE HObtuse]]]].
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
    apply archi__obtuse_case_elimination in archi.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
    apply not_col_permutation_4 in HNCol.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
    destruct (legendre_aux2 archi A B C HNCol HAcute legendre P Q R S T U HDef HGAE) as [B' [C' HInter]].
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
    destruct HInter as [P' [Q' [R' [HOutB [HOutC [HDef' HLea]]]]]].
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
    apply (obtuse_gea_obtuse P' Q' R'), obtuse__nsams in HObtuse; auto.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
    exfalso.
(* Goal: False *)
    apply HObtuse.
(* Goal: @SAMS Tn P' Q' R' P' Q' R' *)
    destruct (legendre_aux1 A B C B' C') as [D' [HInangle [HConga [HCong HTS]]]]; trivial.
(* Goal: @SAMS Tn P' Q' R' P' Q' R' *)
    assert (HNCol' : ~ Col A B' C') by (destruct HTS; Col).
(* Goal: @SAMS Tn P' Q' R' P' Q' R' *)
    destruct (legendre D' HInangle) as [B'' [C'' [HOutB' [HOutC' HBet]]]].
(* Goal: @SAMS Tn P' Q' R' P' Q' R' *)
    assert_diffs.
(* Goal: @SAMS Tn P' Q' R' P' Q' R' *)
    destruct (ex_defect A B'' C'') as [S' [T' [U' HDef'']]]; auto.
(* Goal: not (@eq (@Tpoint Tn) B'' C'') *)
(* Goal: @SAMS Tn P' Q' R' P' Q' R' *)
      intro; subst; apply HNCol; ColR.
(* Goal: @SAMS Tn P' Q' R' P' Q' R' *)
    destruct (ex_suma P' Q' R' P' Q' R') as [V [W [X HSuma]]]; auto.
    destruct (legendre_aux archi A B' C' D' B'' C'' P' Q' R' S' T' U' V W X); trivial;
    [apply l6_7 with B|apply l6_7 with C]; trivial; apply l6_6; trivial.
Qed.

Theorem legendre_s_fourth_theorem :
  archimedes_axiom ->
  legendre_s_parallel_postulate ->
  postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights.
Proof.
(* Goal: forall (_ : @archimedes_axiom Tn) (_ : @legendre_s_parallel_postulate Tn), @postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn *)
  assert (H:=legendre_s_fourth_theorem_aux).
(* Goal: forall (_ : @archimedes_axiom Tn) (_ : @legendre_s_parallel_postulate Tn), @postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn *)
  assert (I:=rah__triangle).
(* Goal: forall (_ : @archimedes_axiom Tn) (_ : @legendre_s_parallel_postulate Tn), @postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn *)
  assert (J:=triangle__existential_triangle); tauto.
Qed.

End Legendre.