Require Export GeoCoq.Tarski_dev.Ch12_parallel.
Require Export GeoCoq.Tarski_dev.Annexes.suma.

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

Section Saccheri.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma sac_perm : forall A B C D, Saccheri A B C D -> Saccheri D C B A.
Proof.
(* Goal: forall (_ : @Bet Tn B C R) (_ : @Bet Tn A D S) (_ : not (@eq (@Tpoint Tn) C R)) (_ : @Per Tn A S R) (_ : @Obtuse Tn A B C), @Lt Tn R S A B *)
  intros.
(* Goal: @Cong Tn B C B' C' *)
  unfold Saccheri in *.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: and (@Per Tn C D A) (and (@Per Tn D A B) (and (@Cong Tn D C B A) (@OS Tn D A C B))) *)
  repeat split; Perp; Cong; Side.
Qed.

Lemma sac_distincts : forall A B C D,
  Saccheri A B C D ->
  A <> B /\ B <> C /\ C <> D /\ A <> D /\ A <> C /\ B <> D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D), iff (@LtA Tn B D C A B D) (@Obtuse Tn A B C) *)
  intros A B C D HSac.
(* Goal: @LtA Tn A C D B A C *)
  unfold Saccheri in HSac.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @LtA Tn B C D A B C *)
  assert(~ Col A D B) by (apply (one_side_not_col123 _ _ _ C); auto).
(* Goal: @LtA Tn B C D A B C *)
  assert(~ Col A D C) by (apply (one_side_not_col123 _ _ _ B); Side).
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @SAMS Tn B C A A C D *)
  repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) B C) *)
  intro; treat_equalities.
(* Goal: False *)
  assert(A=D) by (apply (l8_7 B A D); Perp); auto.
Qed.

Lemma lam_perm : forall A B C D, Lambert A B C D -> Lambert A D C B.
Proof.
(* Goal: forall (_ : @Bet Tn B C R) (_ : @Bet Tn A D S) (_ : not (@eq (@Tpoint Tn) C R)) (_ : @Per Tn A S R) (_ : @Obtuse Tn A B C), @Lt Tn R S A B *)
  intros.
(* Goal: False *)
  unfold Lambert in *.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: and (not (@eq (@Tpoint Tn) A D)) (and (not (@eq (@Tpoint Tn) D C)) (and (not (@eq (@Tpoint Tn) C B)) (and (not (@eq (@Tpoint Tn) A B)) (and (@Per Tn D A B) (and (@Per Tn A B C) (and (@Per Tn A D C) (@Coplanar Tn A D C B))))))) *)
  repeat split; Perp; Cop.
Qed.

(** The two following lemmas come from Theorem 21.10 *)

Lemma sac__cong : forall A B C D, Saccheri A B C D -> Cong A C B D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D), iff (@LtA Tn B D C A B D) (@Obtuse Tn A B C) *)
  intros A B C D HSac.
(* Goal: @LtA Tn B D C A B D *)
  assert(Hdiff := sac_distincts A B C D HSac).
(* Goal: @LtA Tn A C D B A C *)
  unfold Saccheri in HSac.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @Cong Tn A C B D *)
  assert(HSAS := l11_49 B A D C D A).
(* Goal: @Perp Tn B C M N *)
  destruct HSAS; Cong.
(* Goal: @CongA Tn B A D C D A *)
    apply l11_16; Perp.
Qed.

Lemma sac__conga : forall A B C D, Saccheri A B C D -> CongA A B C B C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D), iff (@LtA Tn B D C A B D) (@Obtuse Tn A B C) *)
  intros A B C D HSac.
(* Goal: @LtA Tn B D C A B D *)
  assert(Hdiff := sac_distincts A B C D HSac).
(* Goal: @CongA Tn A B C B C D *)
  assert(HCong := sac__cong A B C D HSac).
(* Goal: @LtA Tn A C D B A C *)
  unfold Saccheri in HSac.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @CongA Tn A B C B C D *)
  assert(HSSS := l11_51 A B C D C B).
(* Goal: @CongA Tn A B D B D C *)
  destruct HSSS as [_ []]; Cong; CongA.
Qed.


Lemma lam__os : forall A B C D, Lambert A B C D -> OS A B C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Lambert Tn A B C D), iff (@Obtuse Tn B C D) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intros A B C D HLam.
(* Goal: @LtA Tn A C D B A C *)
  unfold Lambert in HLam; spliter.
(* Goal: @OS Tn A B C D *)
  assert(HNCol : ~ Col A B C) by (apply per_not_col; trivial).
(* Goal: @OS Tn A B C D *)
  apply l12_6, par_not_col_strict with C; Col.
(* Goal: @Par Tn A B C D *)
  apply l12_9 with A D; Perp; Cop.
Qed.

Lemma per2_os__ncol123 : forall A B C D, Per B A D -> Per A D C -> OS A D B C ->
   ~ Col A B C.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Per Tn B A D) (_ : @Per Tn A D C) (_ : @OS Tn A D B C), not (@Col Tn B C D) *)
  intros A B C D HPer1 HPer2 Hos.
(* Goal: @LtA Tn B C D A B C *)
  assert(~ Col A D B) by (apply (one_side_not_col123 _ _ _ C); auto).
(* Goal: @LtA Tn B C D A B C *)
  assert(~ Col A D C) by (apply (one_side_not_col123 _ _ _ B); Side).
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: not (@Col Tn A B C) *)
  apply (par_strict_not_col_1 _ _ _ D).
(* Goal: @Par_strict Tn A B C D *)
  apply (par_not_col_strict _ _ _ _ D); Col.
(* Goal: @Par Tn A B C D *)
(* Goal: not (@Col Tn A B C) *)
  apply (l12_9 _ _ _ _ A D); Perp; Cop.
Qed.

Lemma per2_os__ncol234 : forall A B C D,
  Per B A D -> Per A D C ->
  OS A D B C ->
  ~ Col B C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Per Tn B A D) (_ : @Per Tn A D C) (_ : @OS Tn A D B C), not (@Col Tn B C D) *)
  intros A B C D HPer1 HPer2 Hos.
(* Goal: @LtA Tn B C D A B C *)
  assert(~ Col A D B) by (apply (one_side_not_col123 _ _ _ C); auto).
(* Goal: @LtA Tn B C D A B C *)
  assert(~ Col A D C) by (apply (one_side_not_col123 _ _ _ B); Side).
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: not (@Col Tn B C D) *)
  apply (par_strict_not_col_2 A).
(* Goal: @Par_strict Tn A B C D *)
  apply (par_not_col_strict _ _ _ _ D); Col.
(* Goal: @Par Tn A B C D *)
(* Goal: not (@Col Tn A B C) *)
  apply (l12_9 _ _ _ _ A D); Perp; Cop.
Qed.

Lemma sac__ncol123 : forall A B C D, Saccheri A B C D -> ~ Col A B C.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D), iff (@LtA Tn B D C A B D) (@Obtuse Tn A B C) *)
  intros A B C D HSac.
(* Goal: @LtA Tn A C D B A C *)
  unfold Saccheri in HSac.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: not (@Col Tn A B C) *)
  apply (per2_os__ncol123 _ _ _ D); assumption.
Qed.

Lemma sac__ncol124 : forall A B C D, Saccheri A B C D -> ~ Col A B D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D), iff (@LtA Tn B D C A B D) (@Obtuse Tn A B C) *)
  intros A B C D HSac.
(* Goal: @LtA Tn A C D B A C *)
  unfold Saccheri in HSac.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: not (@Col Tn A C D) *)
  apply not_col_permutation_1.
(* Goal: not (@Col Tn A D G0) *)
  apply (one_side_not_col123 _ _ _ C); Side.
Qed.

Lemma sac__ncol134 : forall A B C D, Saccheri A B C D -> ~ Col A C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D), iff (@LtA Tn B D C A B D) (@Obtuse Tn A B C) *)
  intros A B C D HSac.
(* Goal: @LtA Tn A C D B A C *)
  unfold Saccheri in HSac.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: not (@Col Tn A C D) *)
  apply not_col_permutation_1.
(* Goal: not (@Col Tn D A C) *)
  apply (one_side_not_col123 _ _ _ B); Side.
Qed.

Lemma sac__ncol234 : forall A B C D, Saccheri A B C D -> ~ Col B C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D), iff (@LtA Tn B D C A B D) (@Obtuse Tn A B C) *)
  intros A B C D HSac.
(* Goal: @LtA Tn A C D B A C *)
  unfold Saccheri in HSac.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: not (@Col Tn B C D) *)
  apply (per2_os__ncol234 A); assumption.
Qed.

Lemma sac__coplanar : forall A B C D, Saccheri A B C D -> Coplanar A B C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D), @Coplanar Tn A B C D *)
  intros A B C D [_ [_ [_ HOS]]].
(* Goal: @Coplanar Tn A B C D *)
  apply os__coplanar in HOS; Cop.
Qed.

(** The five following lemmas come from Theorem 21.8 *)

Lemma lt_os_per2__lta : forall A B C D,
  Per B A D -> Per A D C ->
  OS A D B C ->
  Lt A B C D ->
  LtA B C D A B C.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Per Tn B A D) (_ : @Per Tn A D C) (_ : @OS Tn A D B C) (_ : @Lt Tn A B C D), @LtA Tn B C D A B C *)
  intros A B C D HPer1 HPer2 Hos Hlt.
(* Goal: @LtA Tn B C D A B C *)
  apply lt_right_comm in Hlt.
(* Goal: @LtA Tn B C D A B C *)
  destruct Hlt as [[E []] HNCong].
(* Goal: @LtA Tn B C D A B C *)
  assert(E<>C) by (intro; subst; auto).
(* Goal: @LtA Tn B C D A B C *)
  assert(~ Col A D B) by (apply (one_side_not_col123 _ _ _ C); auto).
(* Goal: @LtA Tn B C D A B C *)
  assert(~ Col A D C) by (apply (one_side_not_col123 _ _ _ B); Side).
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
  assert(HNCol1 :=  per2_os__ncol123 A B C D HPer1 HPer2 Hos).
  assert(HNCol2 :=  per2_os__ncol234 A B C D HPer1 HPer2 Hos).
(* Goal: @LtA Tn B C D A B C *)
  assert(HSac : Saccheri A B E D).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { repeat split; Cong.
(* Goal: @Per Tn N M K *)
(* Goal: @Coplanar Tn N M K H *)
    apply (per_col _ _ C); Col.
(* Goal: @OS Tn A D B E *)
    apply (one_side_transitivity _ _ _ C); auto.
(* Goal: @OS Tn A D C E *)
    apply one_side_symmetry; apply invert_one_side.
(* Goal: @OS Tn I B S R *)
    apply out_one_side.
(* Goal: or (not (@Col Tn D A E)) (not (@Col Tn D A C)) *)
(* Goal: @Out Tn D E C *)
    right; Col.
(* Goal: @Out Tn S R I *)
    apply bet_out; auto.
  }
(* Goal: @LtA Tn B C D A B C *)
  assert(~ Col E C B) by (intro; apply HNCol2; ColR).
(* Goal: @LtA Tn B C D A B C *)
  assert(Par_strict A B C D).
(* Goal: @Par_strict Tn A B C D *)
  { apply (par_not_col_strict _ _ _ _ D); Col.
(* Goal: @Par Tn A B C D *)
(* Goal: not (@Col Tn A B C) *)
    apply (l12_9 _ _ _ _ A D); Perp; Cop.
  }
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @LtA Tn B C D A B C *)
  apply (lta_trans _ _ _ B E D).
  - assert(HInter := l11_41 E C B D).
(* Goal: @LtA Tn B C D B E D *)
    destruct HInter; Between.
(* Goal: @LtA Tn B C D B E D *)
    apply (conga_preserves_lta E C B B E D); try (apply conga_refl); auto.
(* Goal: @CongA Tn E C B B C D *)
    apply (out_conga E C B B C E); try (apply out_trivial); CongA.
(* Goal: @Out Tn C B C' *)
    apply bet_out; Between.

  - apply (conga_preserves_lta A B E A B C); try (apply conga_refl); auto.
(* Goal: @CongA Tn A B E B E D *)
(* Goal: @LtA Tn A B E A B C *)
    apply sac__conga; auto.
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
    split.
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { exists E.
(* Goal: and (@CongA Tn A' A B A' A B) (and (not (@OS Tn A A' C B)) (and (not (@TS Tn C A A' B)) (@Coplanar Tn C A A' B))) *)
      split; CongA.
(* Goal: @InAngle Tn C S I B *)
      apply os2__inangle.
      - apply l12_6.
(* Goal: @Par_strict Tn B A C E *)
        apply (par_strict_col_par_strict _ _ _ D); Par; Col.

      - apply (one_side_transitivity _ _ _ D);
        [|apply invert_one_side; apply one_side_symmetry; apply out_one_side; Col;
          apply bet_out; Between].
(* Goal: @OS Tn B C A D *)
        apply cop__not_two_sides_one_side; Col; Cop.
(* Goal: not (@TS Tn B C A D) *)
        intro Hts.
(* Goal: False *)
        destruct Hts as [_ [_ [I []]]].
(* Goal: @LeA Tn D E F C A B' *)
        assert_diffs.
(* Goal: False *)
        assert(~ OS A D B C); auto.
(* Goal: not (@OS Tn C M A B) *)
        apply l9_9.
(* Goal: @TS Tn P Q B C *)
        repeat split; Col.
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A D) (@Bet Tn B T C)) *)
        exists I.
(* Goal: and (@Col Tn I A D) (@Bet Tn B I C) *)
        split; Col.
(* Goal: @Bet Tn B I C *)
        assert(A<>I) by (intro; subst; assert_cols; Col).
(* Goal: @Bet Tn B I C *)
        assert(D<>I) by (intro; subst; assert_cols; Col).
(* Goal: @Bet Tn B I C *)
        apply out2__bet.
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
        { apply (col_one_side_out _ A); Col.
(* Goal: @OS Tn M N C K *)
          apply (one_side_transitivity _ _ _ D).
(* Goal: @Out Tn S R I *)
          apply invert_one_side; apply out_one_side; Col; apply bet_out; auto.
(* Goal: @OS Tn M N C D *)
(* Goal: @OS Tn M N D K *)
          apply l12_6; Par.
        }
(* Goal: @Out Tn C K M *)
        apply (col_one_side_out _ D); Col.
(* Goal: @OS Tn C D B I *)
        apply (one_side_transitivity _ _ _ A).
(* Goal: @OS Tn M N C D *)
(* Goal: @OS Tn M N D K *)
        apply l12_6; Par.
(* Goal: @Out Tn C B C' *)
        apply invert_one_side; apply one_side_symmetry; apply out_one_side; Col; apply bet_out; Between.
    }
(* Goal: forall _ : @Obtuse Tn A C B, hypothesis_of_obtuse_saccheri_quadrilaterals *)
    intro.
(* Goal: False *)
    assert(HUn := conga_cop__or_out_ts A B E C).
(* Goal: False *)
    destruct HUn; auto.
(* Goal: @Coplanar Tn A B E C *)
(* Goal: False *)
(* Goal: False *)
      apply col_cop__cop with D; Col; apply sac__coplanar, HSac.
(* Goal: False *)
(* Goal: False *)
      assert_cols; Col.
(* Goal: False *)
    assert(~ TS A B E C); auto.
(* Goal: not (@TS Tn I C R D) *)
    apply l9_9_bis.
(* Goal: @OS Tn K H C D *)
    apply l12_6.
(* Goal: @Par_strict Tn A B E C *)
    apply par_strict_right_comm; apply (par_strict_col_par_strict _ _ _ D); Col.
Qed.

Lemma lt4321_os_per2__lta : forall A B C D,
  Per B A D -> Per A D C ->
  OS A D B C -> Lt D C B A ->
  LtA A B C B C D.
Proof.
(* Goal: forall (_ : @Bet Tn B C R) (_ : @Bet Tn A D S) (_ : not (@eq (@Tpoint Tn) C R)) (_ : @Per Tn A S R) (_ : @Obtuse Tn A B C), @Lt Tn R S A B *)
  intros.
(* Goal: @LtA Tn A B C B C D *)
  apply lta_comm, lt_os_per2__lta; Perp; Side.
Qed.

Lemma lta_os_per2__lt : forall A B C D,
  Per B A D -> Per A D C ->
  OS A D B C -> LtA B C D A B C ->
  Lt A B C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Per Tn B A D) (_ : @Per Tn A D C) (_ : @OS Tn A D B C) (_ : @LtA Tn B C D A B C), @Lt Tn A B C D *)
  intros A B C D HPer1 HPer2 Hos HLtA.
(* Goal: @Cong Tn A B C D *)
  destruct (or_lt_cong_gt A B C D) as [Hlt | [Hlt | Hcong]]; trivial; exfalso.
  - unfold Gt in Hlt.
(* Goal: False *)
    apply lt_comm in Hlt.
(* Goal: False *)
    apply (not_and_lta B C D A B C).
(* Goal: and (@Per Tn A D C) (@GtA Tn B C D A D C) *)
    split; trivial.
(* Goal: @LtA Tn A B C B C D *)
    apply lt4321_os_per2__lta; trivial.
  - destruct HLtA as [HLeA HNCongA].
(* Goal: False *)
    apply HNCongA.
(* Goal: @CongA Tn B C D A B C *)
    apply conga_sym, sac__conga.
(* Goal: @Saccheri Tn A B C D *)
    unfold Saccheri; repeat (split; trivial).
Qed.

Lemma lta123234_os_per2__lt : forall A B C D,
  Per B A D -> Per A D C ->
  OS A D B C -> LtA A B C B C D ->
  Lt D C B A.
Proof.
(* Goal: forall (_ : @Bet Tn B C R) (_ : @Bet Tn A D S) (_ : not (@eq (@Tpoint Tn) C R)) (_ : @Per Tn A S R) (_ : @Obtuse Tn A B C), @Lt Tn R S A B *)
  intros.
(* Goal: @Lt Tn D C B A *)
  apply lta_os_per2__lt; Perp; Side.
(* Goal: @LtA Tn C B A D C B *)
  apply lta_comm; trivial.
Qed.

Lemma conga_per2_os__cong : forall A B C D,
  Per B A D -> Per A D C ->
  OS A D B C -> CongA B C D A B C ->
  Cong A B C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Per Tn B A D) (_ : @Per Tn A D C) (_ : @OS Tn A D B C) (_ : @CongA Tn B C D A B C), @Cong Tn A B C D *)
  intros A B C D HPer1 HPer2 Hos HCongA.
(* Goal: @Cong Tn A B C D *)
  destruct (or_lt_cong_gt A B C D) as [Hlt | [Hlt | Hcong]]; trivial; exfalso.
  - destruct (lt_os_per2__lta A B C D); auto.
  - unfold Gt in Hlt.
(* Goal: False *)
    apply lt_comm in Hlt.
(* Goal: False *)
    destruct (lt4321_os_per2__lta A B C D); CongA.
Qed.

(** The two following lemmas constitute Theorem 21.11 *)

Lemma mid2_sac__perp_lower : forall A B C D M N,
  Saccheri A B C D ->
  Midpoint M B C -> Midpoint N A D ->
  Perp A D M N.
Proof.
(* Goal: forall (A B C D M N : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Midpoint Tn M B C) (_ : @Midpoint Tn N A D), @Lambert Tn N M C D *)
  intros A B C D M N HSac HM HN.
(* Goal: @LtA Tn B D C A B D *)
  assert(Hdiff := sac_distincts A B C D HSac).
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(HConga := sac__conga A B C D HSac).
(* Goal: @LtA Tn A C D B A C *)
  unfold Saccheri in HSac.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @Perp Tn B C M N *)
  assert(~ Col A D C) by (apply per_not_col; auto).
(* Goal: @Par_strict Tn A D B C *)
  assert(~ Col B A D) by (apply per_not_col; auto).
(* Goal: @Perp Tn A D M N *)
  assert(HSAS := l11_49 M B A M C D).
(* Goal: @Perp Tn B C M N *)
  destruct HSAS; Cong.
(* Goal: @Out Tn C B C' *)
    apply (out_conga C B A B C D); try (apply out_trivial); CongA; apply l6_6; apply bet_out; Between.
(* Goal: @Perp Tn A D M N *)
  apply (l8_16_2 _ _ _ A); Col.
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { intro.
(* Goal: False *)
    assert(~ OS A D B C); auto.
(* Goal: not (@OS Tn C M A B) *)
    apply l9_9.
(* Goal: @TS Tn P Q B C *)
    repeat split; Col.
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T C M) (@Bet Tn A T B)) *)
    exists M.
(* Goal: and (@Col Tn M C M) (@Bet Tn A M B) *)
    split; Col; Between.
  }
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Per Tn B C C') (@GtA Tn P Q R B C C')) *)
  exists D.
(* Goal: and (@SumA Tn C A B A B C D E F) (@SumA Tn D E F B C A D E D') *)
  split; auto.
Qed.

Lemma mid2_sac__perp_upper : forall A B C D M N, Saccheri A B C D ->
  Midpoint M B C -> Midpoint N A D -> Perp B C M N.
Proof.
(* Goal: forall (A B C D M N : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Midpoint Tn M B C) (_ : @Midpoint Tn N A D), @Lambert Tn N M C D *)
  intros A B C D M N HSac HM HN.
(* Goal: @LtA Tn B D C A B D *)
  assert(Hdiff := sac_distincts A B C D HSac).
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(HConga := sac__conga A B C D HSac).
(* Goal: @LtA Tn A C D B A C *)
  unfold Saccheri in HSac.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @Perp Tn B C M N *)
  assert(~ Col A D C) by (apply per_not_col; auto).
(* Goal: @Par_strict Tn A D B C *)
  assert(~ Col B A D) by (apply per_not_col; auto).
(* Goal: @Perp Tn B C M N *)
  assert(HSAS := l11_49 N A B N D C).
(* Goal: @Perp Tn B C M N *)
  destruct HSAS; Cong.
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { apply l11_16; auto.
(* Goal: @Per Tn N A B *)
    apply (l8_3 D); Perp; Col.
(* Goal: @Per Tn N H G *)
    apply (l8_3 A); Col.
  }
(* Goal: @Perp Tn B C M N *)
  apply perp_right_comm.
(* Goal: @Perp Tn B C N M *)
  apply (l8_16_2 _ _ _ B); Col.
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { intro.
(* Goal: False *)
    assert(Midpoint N B C) by (apply l7_20_bis; Col).
(* Goal: False *)
    assert(~ OS A D B C); auto.
(* Goal: not (@OS Tn C M A B) *)
    apply l9_9.
(* Goal: @TS Tn P Q B C *)
    repeat split; Col.
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A D) (@Bet Tn B T C)) *)
    exists N.
(* Goal: and (@Col Tn M C M) (@Bet Tn A M B) *)
    split; Col; Between.
  }
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Per Tn B B' C') (@GtA Tn P Q R B B' C'))) *)
  exists C.
(* Goal: and (@SumA Tn C A B A B C D E F) (@SumA Tn D E F B C A D E D') *)
  split; auto.
Qed.

Lemma sac__par_strict1423 : forall A B C D, Saccheri A B C D -> Par_strict A D B C.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D), iff (@LtA Tn B D C A B D) (@Obtuse Tn A B C) *)
  intros A B C D HSac.
(* Goal: @Acute Tn A' B' C' *)
  assert(HM := midpoint_existence B C).
(* Goal: iff (@Lt Tn B C A D) (@Obtuse Tn A B C) *)
  destruct HM as [M HM].
(* Goal: @Acute Tn A' B' C' *)
  assert(HN := midpoint_existence A D).
(* Goal: iff (@Lt Tn B C A D) (@Obtuse Tn A B C) *)
  destruct HN as [N HN].
(* Goal: and (not (@eq (@Tpoint Tn) N M)) (and (not (@eq (@Tpoint Tn) M B)) (and (not (@eq (@Tpoint Tn) B A)) (and (not (@eq (@Tpoint Tn) N A)) (and (@Per Tn M N A) (and (@Per Tn N A B) (and (@Per Tn N M B) (@Coplanar Tn N M B A))))))) *)
  assert(HPerp1 := mid2_sac__perp_lower A B C D M N HSac HM HN).
(* Goal: and (not (@eq (@Tpoint Tn) N M)) (and (not (@eq (@Tpoint Tn) M B)) (and (not (@eq (@Tpoint Tn) B A)) (and (not (@eq (@Tpoint Tn) N A)) (and (@Per Tn M N A) (and (@Per Tn N A B) (and (@Per Tn N M B) (@Coplanar Tn N M B A))))))) *)
  assert(HPerp2 := mid2_sac__perp_upper A B C D M N HSac HM HN).
(* Goal: and (not (@eq (@Tpoint Tn) N M)) (and (not (@eq (@Tpoint Tn) M B)) (and (not (@eq (@Tpoint Tn) B A)) (and (not (@eq (@Tpoint Tn) N A)) (and (@Per Tn M N A) (and (@Per Tn N A B) (and (@Per Tn N M B) (@Coplanar Tn N M B A))))))) *)
  assert (~ Col A B C) by (apply sac__ncol123 with D, HSac).
(* Goal: @LtA Tn A C D B A C *)
  unfold Saccheri in HSac.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @Par_strict Tn A D B C *)
  assert (~ Col B A D) by (apply per_not_col; auto).
(* Goal: @Par_strict Tn A D B C *)
  assert (Coplanar A B C A) by (exists A; left; split; Col).
(* Goal: @Par_strict Tn A D B C *)
  assert (Coplanar A B C B) by (exists B; left; split; Col).
(* Goal: @Par_strict Tn A D B C *)
  assert (Coplanar A B C C) by (exists C; right; left; split; Col).
(* Goal: @Par_strict Tn A D B C *)
  assert (Coplanar A B C D) by Cop.
(* Goal: @Par_strict Tn A D B C *)
  assert (Coplanar A B C M) by (exists B; left; split; Col).
(* Goal: @Par_strict Tn A D B C *)
  assert (Coplanar A B C N).
(* Goal: @Coplanar Tn A B C N *)
(* Goal: @Par_strict Tn A D B C *)
    apply coplanar_perm_12, col_cop__cop with D; Col; Cop.
(* Goal: @Par_strict Tn A B C D *)
  apply (par_not_col_strict _ _ _ _ C); Col.
(* Goal: @Par Tn A D B C *)
(* Goal: not (@Col Tn A D C) *)
    apply (l12_9 _ _ _ _ M N); auto; apply coplanar_pseudo_trans with A B C; assumption.
(* Goal: not (@Col Tn M N H) *)
    apply per_not_col; auto.
Qed.

Lemma sac__par_strict1234 : forall A B C D, Saccheri A B C D -> Par_strict A B C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D), iff (@LtA Tn B D C A B D) (@Obtuse Tn A B C) *)
  intros A B C D HSac.
(* Goal: @Par_strict Tn A B C D *)
  apply par_not_col_strict with C; Col; [|apply sac__ncol123 with D; trivial].
(* Goal: @LtA Tn A C D B A C *)
  assert (Hd := sac_distincts A B C D HSac); unfold Saccheri in HSac; spliter.
(* Goal: @Par Tn A B C D *)
  apply l12_9 with A D; Perp; Cop.
Qed.

Lemma sac__par1423 : forall A B C D, Saccheri A B C D -> Par A D B C.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D), iff (@LtA Tn B D C A B D) (@Obtuse Tn A B C) *)
  intros A B C D HSac.
(* Goal: @Par Tn A D B C *)
  apply par_strict_par, sac__par_strict1423, HSac.
Qed.

Lemma sac__par1234 : forall A B C D, Saccheri A B C D -> Par A B C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D), iff (@LtA Tn B D C A B D) (@Obtuse Tn A B C) *)
  intros A B C D HSac.
(* Goal: @Par Tn A B C D *)
  apply par_strict_par, sac__par_strict1234, HSac.
Qed.

Lemma lam__par_strict1234 : forall A B C D, Lambert A B C D -> Par_strict A B C D.
Proof.
(* Goal: @Lambert Tn N M B A *)
  unfold Lambert.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Lambert Tn A B C D), iff (@Obtuse Tn B C D) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intros A B C D HLam.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @Par_strict Tn A B C D *)
  apply (par_not_col_strict _ _ _ _ C); Col.
(* Goal: @Par Tn A B C D *)
(* Goal: not (@Col Tn A B C) *)
    apply (l12_9 _ _ _ _ A D); Perp; Cop.
(* Goal: not (@Col Tn M N H) *)
  apply per_not_col; auto.
Qed.

Lemma lam__par_strict1423 : forall A B C D, Lambert A B C D -> Par_strict A D B C.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Lambert Tn A B C D), @Par_strict Tn A D B C *)
  intros; apply par_strict_right_comm, lam__par_strict1234, lam_perm; assumption.
Qed.

Lemma lam__par1234 : forall A B C D, Lambert A B C D -> Par A B C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Lambert Tn A B C D), iff (@Obtuse Tn B C D) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intros A B C D HLam.
(* Goal: @Par Tn A B C D *)
  apply par_strict_par, lam__par_strict1234, HLam.
Qed.

Lemma lam__par1423 : forall A B C D, Lambert A B C D -> Par A D B C.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Lambert Tn A B C D), iff (@Obtuse Tn B C D) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intros A B C D HLam.
(* Goal: @Par Tn A D B C *)
  apply par_strict_par, lam__par_strict1423, HLam.
Qed.

(** The four following constitute Theorem 22.3 *)

Lemma mid2_sac__lam6521 : forall A B C D M N,
  Saccheri A B C D ->
  Midpoint M B C -> Midpoint N A D ->
  Lambert N M B A.
Proof.
(* Goal: forall (A B C D M N : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Midpoint Tn M B C) (_ : @Midpoint Tn N A D), @Lambert Tn N M C D *)
  intros A B C D M N HSac HM HN.
(* Goal: @Lambert Tn N M B A *)
  unfold Lambert.
(* Goal: @LtA Tn B D C A B D *)
  assert(Hdiff := sac_distincts A B C D HSac).
(* Goal: and (not (@eq (@Tpoint Tn) N M)) (and (not (@eq (@Tpoint Tn) M B)) (and (not (@eq (@Tpoint Tn) B A)) (and (not (@eq (@Tpoint Tn) N A)) (and (@Per Tn M N A) (and (@Per Tn N A B) (and (@Per Tn N M B) (@Coplanar Tn N M B A))))))) *)
  assert(HPerp1 := mid2_sac__perp_lower A B C D M N HSac HM HN).
(* Goal: and (not (@eq (@Tpoint Tn) N M)) (and (not (@eq (@Tpoint Tn) M B)) (and (not (@eq (@Tpoint Tn) B A)) (and (not (@eq (@Tpoint Tn) N A)) (and (@Per Tn M N A) (and (@Per Tn N A B) (and (@Per Tn N M B) (@Coplanar Tn N M B A))))))) *)
  assert(HPerp2 := mid2_sac__perp_upper A B C D M N HSac HM HN).
(* Goal: and (not (@eq (@Tpoint Tn) N M)) (and (not (@eq (@Tpoint Tn) M B)) (and (not (@eq (@Tpoint Tn) B A)) (and (not (@eq (@Tpoint Tn) N A)) (and (@Per Tn M N A) (and (@Per Tn N A B) (and (@Per Tn N M B) (@Coplanar Tn N M B A))))))) *)
  assert (~ Col A B C) by (apply sac__ncol123 with D, HSac).
(* Goal: @LtA Tn A C D B A C *)
  unfold Saccheri in HSac.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @SAMS Tn B C A A C D *)
  repeat split; auto.
  - apply perp_per_1; auto.
(* Goal: @Perp Tn N M A N *)
    apply (perp_col1 _ _ _ D); Perp; Col.
  - apply (l8_3 D); Perp; Col.
  - apply perp_per_1; auto.
(* Goal: @Perp Tn M N B M *)
    apply (perp_col1 _ _ _ C); Perp; Col.
  - apply coplanar_perm_5, col_cop__cop with C; Col.
(* Goal: @Coplanar Tn S A B C *)
    apply coplanar_perm_22, col_cop__cop with D; Col; Cop.
Qed.

Lemma mid2_sac__lam6534 : forall A B C D M N,
  Saccheri A B C D ->
  Midpoint M B C -> Midpoint N A D ->
  Lambert N M C D.
Proof.
(* Goal: forall (A B C D M N : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Midpoint Tn M B C) (_ : @Midpoint Tn N A D), @Lambert Tn N M C D *)
  intros A B C D M N HSac HM HN.
(* Goal: @Lambert Tn N M C D *)
  apply (mid2_sac__lam6521 _ _ B A); try (apply l7_2); auto.
(* Goal: @Saccheri Tn D C B A *)
  apply sac_perm; auto.
Qed.

Lemma lam6521_mid2__sac : forall A B C D M N,
  Lambert N M B A ->
  Midpoint M B C -> Midpoint N A D ->
  Saccheri A B C D.
Proof.
(* Goal: forall (A B C D M N : @Tpoint Tn) (_ : @Lambert Tn N M C D) (_ : @Midpoint Tn M B C) (_ : @Midpoint Tn N A D), @Saccheri Tn A B C D *)
  intros A B C D M N HLam HM HN.
(* Goal: @Obtuse Tn B C D *)
  assert (HLam' := HLam).
(* Goal: @Obtuse Tn B C D *)
  unfold Lambert in HLam'.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @Saccheri Tn A B C D *)
  assert(Per D A B) by (apply (l8_3 N); Col).
(* Goal: @Saccheri Tn A B C D *)
  assert(ReflectL D A M N).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { split.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Midpoint Tn X A D) (@Col Tn M N X)) *)
(* Goal: or (@Perp Tn M N A D) (@eq (@Tpoint Tn) A D) *)
    exists N; Col.
(* Goal: or (@Perp Tn M N A D) (@eq (@Tpoint Tn) A D) *)
    left; apply (perp_col1 _ _ _ N); Col; Perp.
  }
(* Goal: @Saccheri Tn A B C D *)
  assert(ReflectL A D M N) by (apply l10_4_spec; auto).
(* Goal: @Saccheri Tn A B C D *)
  assert(ReflectL C B M N).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { split.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Midpoint Tn X B C) (@Col Tn M N X)) *)
(* Goal: or (@Perp Tn M N B C) (@eq (@Tpoint Tn) B C) *)
    exists M; Col.
(* Goal: or (@Perp Tn M N B C) (@eq (@Tpoint Tn) B C) *)
    left; apply (perp_col1 _ _ _ M); Col; Perp.
  }
(* Goal: @Saccheri Tn A B C D *)
  assert(ReflectL B C M N) by (apply l10_4_spec; auto).
(* Goal: @SAMS Tn B C A A C D *)
  repeat split; auto.
  - Perp.
  - apply (image_spec_preserves_per D A B _ _ _ M N); auto.
  - apply cong_left_commutativity.
(* Goal: @Cong Tn B A C D *)
    apply (l10_10_spec M N); auto.
  - apply (col_one_side _ N); Col.
(* Goal: @OS Tn K H C D *)
    apply l12_6.
(* Goal: @Par_strict Tn A N B C *)
    apply (par_strict_col_par_strict _ _ _ M); Col.
(* Goal: @Par_strict Tn A N B M *)
    apply lam__par_strict1423 in HLam; Par.
Qed.

Lemma lam6534_mid2__sac : forall A B C D M N,
  Lambert N M C D ->
  Midpoint M B C -> Midpoint N A D ->
  Saccheri A B C D.
Proof.
(* Goal: forall (A B C D M N : @Tpoint Tn) (_ : @Lambert Tn N M C D) (_ : @Midpoint Tn M B C) (_ : @Midpoint Tn N A D), @Saccheri Tn A B C D *)
  intros A B C D M N HLam HM HN.
(* Goal: @Saccheri Tn A B C D *)
  apply sac_perm.
(* Goal: @Saccheri Tn D C B A *)
  apply (lam6521_mid2__sac _ _ _ _ M N); Midpoint.
Qed.

(** The six following lemmas constitute Theorem 22.5 *)

Lemma cong_lam__per : forall A B C D,
  Lambert A B C D ->
  Cong A D B C ->
  Per B C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Lambert Tn A B C D) (_ : @Cong Tn A D B C), @Per Tn B C D *)
  intros A B C D HLam HCong.
(* Goal: @Obtuse Tn B C D *)
  assert (HLam' := HLam).
(* Goal: @Obtuse Tn B C D *)
  unfold Lambert in HLam'.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @Per Tn B C D *)
  apply l8_2, (l11_17 A D C); auto.
(* Goal: @CongA Tn A D C D C B *)
  apply sac__conga.
(* Goal: @Saccheri Tn A D C B *)
  repeat split; Perp; Cong.
(* Goal: @OS Tn A B D C *)
  apply one_side_symmetry, l12_6, lam__par_strict1234, HLam.
Qed.

Lemma lam_lt__acute : forall A B C D,
  Lambert A B C D ->
  Lt A D B C ->
  Acute B C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Lambert Tn A B C D) (_ : @Lt Tn B C A D), @Obtuse Tn B C D *)
  intros A B C D HLam HLt.
(* Goal: @Obtuse Tn B C D *)
  assert (HLam' := HLam).
(* Goal: @Obtuse Tn B C D *)
  unfold Lambert in HLam'.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @SumA Tn I B C B C D A B I *)
  exists A.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Per Tn B C C') (@GtA Tn P Q R B C C')) *)
  exists D.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Per Tn B B' C') (@GtA Tn P Q R B B' C'))) *)
  exists C.
(* Goal: and (@Per Tn A D C) (@GtA Tn B C D A D C) *)
  split; trivial.
(* Goal: @GtA Tn B C D A D C *)
  apply lta_left_comm, lt_os_per2__lta; Perp; [|apply lt_right_comm; trivial].
(* Goal: @OS Tn A B D C *)
  apply one_side_symmetry, l12_6, lam__par_strict1234, HLam.
Qed.

Lemma lam_lt__obtuse : forall A B C D,
  Lambert A B C D ->
  Lt B C A D ->
  Obtuse B C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Lambert Tn A B C D) (_ : @Lt Tn B C A D), @Obtuse Tn B C D *)
  intros A B C D HLam HLt.
(* Goal: @Obtuse Tn B C D *)
  assert (HLam' := HLam).
(* Goal: @Obtuse Tn B C D *)
  unfold Lambert in HLam'.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @SumA Tn I B C B C D A B I *)
  exists A.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Per Tn B C C') (@GtA Tn P Q R B C C')) *)
  exists D.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Per Tn B B' C') (@GtA Tn P Q R B B' C'))) *)
  exists C.
(* Goal: and (@Per Tn A D C) (@GtA Tn B C D A D C) *)
  split; trivial.
(* Goal: @GtA Tn B C D A D C *)
  apply lta_left_comm, lt_os_per2__lta; Perp; [|apply lt_right_comm; trivial].
(* Goal: @OS Tn B A C D *)
  apply invert_one_side, l12_6, lam__par_strict1234, HLam.
Qed.

Lemma lam_per__cong : forall A B C D,
  Lambert A B C D ->
  Per B C D ->
  Cong A D B C.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Lambert Tn A B C D) (_ : @Per Tn B C D), @Cong Tn A D B C *)
  intros A B C D HLam HPer.
(* Goal: @LtA Tn B C D B C D *)
  assert (HL := HLam).
(* Goal: @LtA Tn B C D B C D *)
  ex_and HL Hd.
  destruct (or_lt_cong_gt A D B C) as [Habs|[HCong|Habs]]; trivial;
(* Goal: @Lt Tn A D B C *)
  exfalso; apply (nlta B C D).
  - apply acute_per__lta; trivial.
(* Goal: @Acute Tn B C D *)
    apply (lam_lt__acute A); trivial.
  - apply obtuse_per__lta; trivial.
(* Goal: @Obtuse Tn B C D *)
    apply (lam_lt__obtuse A); trivial.
Qed.

Lemma acute_lam__lt : forall A B C D,
  Lambert A B C D ->
  Acute B C D ->
  Lt A D B C.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Lambert Tn A B C D) (_ : @Acute Tn B C D), @Lt Tn A D B C *)
  intros A B C D HLam HAcute.
(* Goal: @Lt Tn A D B C *)
  destruct (or_lt_cong_gt A D B C) as [|Habs]; trivial.
(* Goal: @Lt Tn A D B C *)
  exfalso; apply (nlta B C D).
(* Goal: False *)
  destruct Habs.
  - apply acute_obtuse__lta; trivial.
(* Goal: @Obtuse Tn B C D *)
    apply (lam_lt__obtuse A); trivial.
  - assert (HL := HLam).
(* Goal: @LtA Tn B C D B C D *)
    ex_and HL Hd.
(* Goal: @LtA Tn B C D B C D *)
    apply acute_per__lta; trivial.
(* Goal: @Per Tn B C D *)
    apply (cong_lam__per A); trivial.
Qed.

Lemma lam_obtuse__lt : forall A B C D,
  Lambert A B C D ->
  Obtuse B C D ->
  Lt B C A D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Lambert Tn A B C D) (_ : @Obtuse Tn B C D), @Lt Tn B C A D *)
  intros A B C D HLam HObtuse.
  destruct (or_lt_cong_gt A D B C) as [Habs|[Habs|HLt]]; trivial;
(* Goal: @Lt Tn A D B C *)
  exfalso; apply (nlta B C D).
  - apply acute_obtuse__lta; trivial.
(* Goal: @Acute Tn B C D *)
    apply (lam_lt__acute A); trivial.
  - assert (HL := HLam).
(* Goal: @LtA Tn B C D B C D *)
    ex_and HL Hd.
(* Goal: @LtA Tn B C D B C D *)
    apply obtuse_per__lta; trivial.
(* Goal: @Per Tn B C D *)
    apply (cong_lam__per A); trivial.
Qed.

(** The three following lemmas constitute Omar Khayyam's Theorem (22.6) *)

Lemma cong_sac__per : forall A B C D,
  Saccheri A B C D ->
  Cong A D B C <-> Per A B C.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D), iff (@LtA Tn B D C A B D) (@Obtuse Tn A B C) *)
  intros A B C D HSac.
(* Goal: @Acute Tn A' B' C' *)
  assert(HM := midpoint_existence B C).
(* Goal: iff (@Lt Tn B C A D) (@Obtuse Tn A B C) *)
  destruct HM as [M HM].
(* Goal: @Acute Tn A' B' C' *)
  assert(HN := midpoint_existence A D).
(* Goal: iff (@Lt Tn B C A D) (@Obtuse Tn A B C) *)
  destruct HN as [N HN].
(* Goal: iff (@Lt Tn B C A D) (@Obtuse Tn A B C) *)
  assert(HLam := mid2_sac__lam6521 A B C D M N HSac HM HN).
(* Goal: @LtA Tn A C D B A C *)
  apply sac_distincts in HSac; spliter.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split.
  - intro HCong.
(* Goal: @Per Tn Q P P' *)
    apply (per_col _ _ M); Col.
(* Goal: @Per Tn A B M *)
    apply l8_2, (cong_lam__per N); auto.
(* Goal: @Cong Tn N A M B *)
    apply cong_commutativity; apply (cong_cong_half_1 _ _ D _ _ C); auto.
  - intro HPer.
(* Goal: @Cong Tn A D B C *)
    apply cong_mid2__cong with N M; trivial.
(* Goal: @Cong Tn A N B M *)
    apply cong_commutativity, lam_per__cong; trivial.
(* Goal: @Per Tn M B A *)
    apply l8_2, per_col with C; Col.
Qed.

Lemma lt_sac__acute : forall A B C D,
  Saccheri A B C D ->
  Lt A D B C <-> Acute A B C.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D), iff (@LtA Tn B D C A B D) (@Obtuse Tn A B C) *)
  intros A B C D HSac.
(* Goal: @Acute Tn A' B' C' *)
  assert(HM := midpoint_existence B C).
(* Goal: iff (@Lt Tn B C A D) (@Obtuse Tn A B C) *)
  destruct HM as [M HM].
(* Goal: @Acute Tn A' B' C' *)
  assert(HN := midpoint_existence A D).
(* Goal: iff (@Lt Tn B C A D) (@Obtuse Tn A B C) *)
  destruct HN as [N HN].
(* Goal: iff (@Lt Tn B C A D) (@Obtuse Tn A B C) *)
  assert(HLam := mid2_sac__lam6521 A B C D M N HSac HM HN).
(* Goal: iff (@Lt Tn B C A D) (@Obtuse Tn A B C) *)
  assert (HCongA : CongA A B C M B A).
(* Goal: @LtA Tn A C D B A C *)
  { apply sac_distincts in HSac; spliter.
(* Goal: @LeA Tn D E F C A B' *)
    assert_diffs.
(* Goal: @CongA Tn A B C M B A *)
    apply conga_right_comm, out2__conga.
(* Goal: @Out Tn B A A *)
(* Goal: @Out Tn B M C *)
      apply out_trivial; auto.
(* Goal: @Out Tn C B C' *)
    apply bet_out; Between.
  }
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split.
  - intro HLt.
(* Goal: @Acute Tn A B C *)
    apply (acute_conga__acute M B A); CongA.
(* Goal: @Acute Tn M B A *)
    apply (lam_lt__acute N); trivial.
(* Goal: @Lt Tn N A M B *)
    apply lt_comm, lt_mid2__lt12 with D C; trivial.
  - intro HAcute.
(* Goal: @Lt Tn A D B C *)
    apply lt_mid2__lt13 with N M; trivial.
(* Goal: @Lt Tn A N B M *)
    apply lt_comm, acute_lam__lt; trivial.
(* Goal: @Acute Tn M B A *)
    apply (acute_conga__acute A B C); trivial.
Qed.

Lemma lt_sac__obtuse : forall A B C D,
  Saccheri A B C D ->
  Lt B C A D <-> Obtuse A B C.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D), iff (@LtA Tn B D C A B D) (@Obtuse Tn A B C) *)
  intros A B C D HSac.
(* Goal: @Acute Tn A' B' C' *)
  assert(HM := midpoint_existence B C).
(* Goal: iff (@Lt Tn B C A D) (@Obtuse Tn A B C) *)
  destruct HM as [M HM].
(* Goal: @Acute Tn A' B' C' *)
  assert(HN := midpoint_existence A D).
(* Goal: iff (@Lt Tn B C A D) (@Obtuse Tn A B C) *)
  destruct HN as [N HN].
(* Goal: iff (@Lt Tn B C A D) (@Obtuse Tn A B C) *)
  assert(HLam := mid2_sac__lam6521 A B C D M N HSac HM HN).
(* Goal: iff (@Lt Tn B C A D) (@Obtuse Tn A B C) *)
  assert (HCongA : CongA A B C M B A).
(* Goal: @LtA Tn A C D B A C *)
  { apply sac_distincts in HSac; spliter.
(* Goal: @LeA Tn D E F C A B' *)
    assert_diffs.
(* Goal: @CongA Tn A B C M B A *)
    apply conga_right_comm, out2__conga.
(* Goal: @Out Tn B A A *)
(* Goal: @Out Tn B M C *)
      apply out_trivial; auto.
(* Goal: @Out Tn C B C' *)
    apply bet_out; Between.
  }
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split.
  - intro HLt.
(* Goal: @Obtuse Tn A B C *)
    apply (conga_obtuse__obtuse M B A); CongA.
(* Goal: @Obtuse Tn M B A *)
    apply (lam_lt__obtuse N); trivial.
(* Goal: @Lt Tn M B N A *)
    apply lt_comm, lt_mid2__lt12 with C D; trivial.
  - intro HObtuse.
(* Goal: @Lt Tn B C A D *)
    apply lt_mid2__lt13 with M N; trivial.
(* Goal: @Lt Tn B M A N *)
    apply lt_comm, lam_obtuse__lt; trivial.
(* Goal: @Obtuse Tn M B A *)
    apply (conga_obtuse__obtuse A B C); trivial.
Qed.


Lemma t22_7__per : forall A B C D P Q,
  Saccheri A B C D ->
  Bet B P C -> Bet A Q D ->
  A <> Q -> B <> P -> P <> C ->
  Per P Q A ->
  Cong P Q A B ->
  Per A B C.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Bet Tn B P C) (_ : @Bet Tn A Q D) (_ : not (@eq (@Tpoint Tn) A Q)) (_ : not (@eq (@Tpoint Tn) B P)) (_ : not (@eq (@Tpoint Tn) P C)) (_ : @Per Tn P Q A) (_ : @Cong Tn P Q A B), @Per Tn A B C *)
  intros A B C D P Q HSac HP HQ HAQ HBP HPC HPerQ HCong.
(* Goal: @Obtuse Tn A B C *)
  assert(HSac' := HSac).
(* Goal: @Obtuse Tn A B C *)
  destruct HSac'.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @Obtuse Tn A B C *)
  assert(HNCol1 : ~ Col A D B) by (apply (one_side_not_col123 _ _ _ C); auto).
(* Goal: @Per Tn A B C *)
  assert(HNCol2 : ~ Col B C D) by (apply (per2_os__ncol234 A); auto).
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @Obtuse Tn A B C *)
  assert(Q <> D).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { intro.
(* Goal: False *)
    subst Q.
(* Goal: False *)
    destruct HSac.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: False *)
    assert(Col C P D).
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
      apply cop_per2__col with A; Perp.
(* Goal: @Coplanar Tn A C R D *)
(* Goal: False *)
      apply coplanar_perm_3, col_cop__cop with B; Col; Cop.
(* Goal: False *)
    apply HNCol2; ColR.
  }
(* Goal: @Per Tn A B C *)
  assert(HSac1 : Saccheri A B P Q).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { repeat split; Cong.
(* Goal: @Per Tn B A S *)
(* Goal: @Per Tn A S I *)
(* Goal: @OS Tn A S B I *)
    apply (per_col _ _ D); Col.
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
    Perp.
    apply (col_one_side _ D); Col;
    apply (l9_17 _ _ C); Between.
  }
(* Goal: @Per Tn A B C *)
  assert(HSac2 : Saccheri D C P Q).
(* Goal: @SAMS Tn B C A A C D *)
  { repeat split; auto.
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
    apply (per_col _ _ A); Col; Perp.
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
    apply (l8_3 A); Col; Perp.
(* Goal: @Cong Tn D C I S *)
(* Goal: @OS Tn D S C I *)
    apply (cong_transitivity _ _ A B); Cong.
(* Goal: @OS Tn D N C G *)
    apply (col_one_side _ A); Col.
(* Goal: @OS Tn D A C P *)
    apply (l9_17 _ _ B); Between; Side.
  }
(* Goal: @Per Tn A B C *)
  apply (bet_suma__per _ _ _ B P C); auto.
(* Goal: @SumA Tn A B C A B C B P C *)
  apply (conga3_suma__suma B P Q Q P C B P C); try (apply conga_refl); auto.
  - exists C.
(* Goal: and (@CongA Tn Q P C Q P C) (and (not (@OS Tn P Q B C)) (and (@Coplanar Tn B P Q C) (@CongA Tn B P C B P C))) *)
    repeat (split; CongA); [|exists C; left; split; Col].
(* Goal: not (@OS Tn C M A B) *)
    apply l9_9.
(* Goal: @TS Tn P Q B C *)
    destruct HSac1.
(* Goal: @TS Tn P Q B C *)
    destruct HSac2.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: @SAMS Tn B C A A C D *)
    repeat split; auto.
(* Goal: not (@Col Tn B P Q) *)
      apply (per2_os__ncol234 A); auto.
(* Goal: not (@Col Tn C P Q) *)
      apply (per2_os__ncol234 D); auto.
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T P Q) (@Bet Tn B T C)) *)
    exists P; Col.

  - apply (out_conga B P Q A B P); try apply (out_trivial); auto.
(* Goal: @CongA Tn A B E B E D *)
(* Goal: @LtA Tn A B E A B C *)
    apply conga_sym; apply sac__conga; auto.
(* Goal: @Out Tn S R I *)
    apply bet_out; auto.

  - apply (conga_trans _ _ _ P C D).
(* Goal: @Saccheri Tn D C B A *)
      apply sac__conga; apply sac_perm; auto.
(* Goal: @CongA Tn P C D A B C *)
    apply (out_conga B C D A B C); try apply (out_trivial); auto.
(* Goal: @CongA Tn A B E B E D *)
(* Goal: @LtA Tn A B E A B C *)
    apply conga_sym; apply sac__conga; auto.
(* Goal: @Out Tn C B C' *)
    apply l6_6; apply bet_out; Between.
Qed.

Lemma t22_7__acute : forall A B C D P Q,
  Saccheri A B C D ->
  Bet B P C -> Bet A Q D ->
  A <> Q -> B <> P -> P <> C ->
  Per P Q A ->
  Lt P Q A B ->
  Acute A B C.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Bet Tn B P C) (_ : @Bet Tn A Q D) (_ : not (@eq (@Tpoint Tn) A Q)) (_ : not (@eq (@Tpoint Tn) B P)) (_ : not (@eq (@Tpoint Tn) P C)) (_ : @Per Tn P Q A) (_ : @Lt Tn A B P Q), @Obtuse Tn A B C *)
  intros A B C D P Q HSac HP HQ HAQ HBP HPC HPerQ Hlt.
(* Goal: @Obtuse Tn A B C *)
  assert(HSac' := HSac).
(* Goal: @Obtuse Tn A B C *)
  destruct HSac'.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @Obtuse Tn A B C *)
  assert(HNCol1 : ~ Col A D B) by (apply (one_side_not_col123 _ _ _ C); auto).
(* Goal: @Obtuse Tn A B C *)
  assert(HNCol2 : ~ Col A B C) by (apply (per2_os__ncol123 _ _ _ D); auto).
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @Obtuse Tn A B C *)
  assert(OS A Q B P) by (apply (col_one_side _ D); Col; apply (l9_17 _ _ C); auto).
(* Goal: @Obtuse Tn A B C *)
  assert(HNCol3 : ~ Col A Q P) by (apply (one_side_not_col123 _ _ _ B); Side).
(* Goal: @Acute Tn A B C *)
  assert(HNCol4 : ~ Col B P Q).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { apply (per2_os__ncol234 A); auto.
(* Goal: @Per Tn B A S *)
(* Goal: @Per Tn A S I *)
(* Goal: @OS Tn A S B I *)
    apply (per_col _ _ D); Col.
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
    Perp.
  }
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @Obtuse Tn A B C *)
  assert(Q <> D).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { intro.
(* Goal: False *)
    subst Q.
(* Goal: False *)
    assert(Haux : ~ Col B C D) by (apply (per2_os__ncol234 A); auto).
(* Goal: False *)
    assert(Col C P D). 
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
      apply cop_per2__col with A; Perp.
(* Goal: @Coplanar Tn A C R D *)
(* Goal: False *)
      apply coplanar_perm_3, col_cop__cop with B; Col; Cop.
(* Goal: False *)
    apply Haux; ColR.
  }
(* Goal: False *)
  assert(HSuma := ex_suma A B C A B C).
(* Goal: False *)
  destruct HSuma as [R [S [T HSuma]]]; auto.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @Acute Tn A B C *)
  assert(Hlta1 : LtA A B C B P Q).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { apply (conga_preserves_lta A B P B P Q); try (apply conga_refl); auto.
(* Goal: @Out Tn S R I *)
      apply (out_conga A B P A B P); try (apply out_trivial); CongA; apply bet_out; auto.
(* Goal: @LtA Tn D C P C P Q *)
    apply lt4321_os_per2__lta; auto.
(* Goal: @Per Tn B A S *)
(* Goal: @Per Tn A S I *)
(* Goal: @OS Tn A S B I *)
    apply (per_col _ _ D); Col.
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
    Perp.
(* Goal: @Lt Tn Q P B A *)
    apply lt_comm; auto.
  }
(* Goal: @Acute Tn A B C *)
  assert(Hlta2 : LtA A B C Q P C).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { apply (conga_preserves_lta D C P C P Q); try (apply conga_pseudo_refl); auto.
    - apply sac__conga in HSac.
(* Goal: @CongA Tn D C M A B C *)
      apply (out_conga D C B A B C); try (apply out_trivial); CongA.
(* Goal: @Out Tn C B C' *)
      apply l6_6; apply bet_out; Between.
    - apply lt4321_os_per2__lta; auto.
(* Goal: @Per Tn C D S *)
(* Goal: @Per Tn D S I *)
(* Goal: @Cong Tn D C I S *)
(* Goal: @OS Tn D S C I *)
      apply (per_col _ _ A); Perp; Col.
(* Goal: @Per Tn D Q P *)
      apply (l8_3 A); Perp; Col.
(* Goal: @OS Tn D A C P *)
      apply (col_one_side _ A); Col; apply (l9_17 _ _ B); Between; Side.
(* Goal: @Lt Tn Q P C D *)
      apply (cong2_lt__lt P Q A B); Cong.
  }
(* Goal: @Acute Tn A B C *)
  assert(~ OS P Q B C).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { apply l9_9.
(* Goal: @TS Tn P Q B C *)
    repeat split; Col.
(* Goal: not (@Col Tn B P Q) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T P Q) (@Bet Tn B T C)) *)
    intro; apply HNCol4; ColR.
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T P Q) (@Bet Tn B T C)) *)
    exists P; Col.
  }
(* Goal: @Acute Tn A B C *)
  assert(SAMS B P Q Q P C).
(* Goal: @SAMS Tn B C A A C D *)
  { repeat split; auto.
(* Goal: or (@Out Tn P Q C) (not (@Bet Tn B P Q)) *)
(* Goal: @ex (@Tpoint Tn) (fun J : @Tpoint Tn => and (@CongA Tn Q P J Q P C) (and (not (@OS Tn P Q B J)) (and (not (@TS Tn B P Q J)) (@Coplanar Tn B P Q J)))) *)
      right; intro; Col.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Per Tn B B' C') (@GtA Tn P Q R B B' C'))) *)
    exists C.
(* Goal: and (@CongA Tn C B A B C D) (and (not (@OS Tn B C I A)) (and (@Coplanar Tn I B C A) (@CongA Tn I B A A B I))) *)
    repeat (split; CongA).
(* Goal: False *)
(* Goal: False *)
      intro Hts; destruct Hts as [_ []]; assert_cols; Col.
(* Goal: and (@Col Tn I A D) (@Bet Tn B I C) *)
    exists C; left; split; Col.
  }
(* Goal: @Acute Tn A B C *)
  assert(SAMS A B C A B C).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { destruct Hlta1.
(* Goal: @SAMS Tn A B C A B C *)
    destruct Hlta2.
(* Goal: @SAMS Tn A B C A B C *)
    apply (sams_lea2__sams _ _ _ _ _ _ B P Q Q P C); auto.
  }
(* Goal: @Acute Tn A B C *)
  apply (nbet_sams_suma__acute _ _ _ R S T); auto.
(* Goal: forall _ : @Obtuse Tn A C B, hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intro.
(* Goal: False *)
  apply (nlta R S T).
(* Goal: @LtA Tn R S T R S T *)
  apply (sams_lta2_suma2__lta A B C A B C _ _ _ B P Q Q P C); auto.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Per Tn B B' C') (@GtA Tn P Q R B B' C'))) *)
  exists C.
(* Goal: and (@CongA Tn A' A B A' A B) (and (not (@OS Tn A A' C B)) (and (not (@TS Tn C A A' B)) (@Coplanar Tn C A A' B))) *)
  split; CongA.
(* Goal: and (@SumA Tn C A B A B C D E F) (@SumA Tn D E F B C A D E D') *)
  split; auto.
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split.
(* Goal: and (@Col Tn I A D) (@Bet Tn B I C) *)
    exists C; left; split; Col.
(* Goal: @CongA Tn B A' C P Q R *)
(* Goal: @LtA Tn P Q R B A' C *)
  apply conga_line; auto.
Qed.

Lemma t22_7__obtuse : forall A B C D P Q,
  Saccheri A B C D ->
  Bet B P C -> Bet A Q D ->
  A <> Q -> B <> P -> P <> C ->
  Per P Q A ->
  Lt A B P Q ->
  Obtuse A B C.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Bet Tn B P C) (_ : @Bet Tn A Q D) (_ : not (@eq (@Tpoint Tn) A Q)) (_ : not (@eq (@Tpoint Tn) B P)) (_ : not (@eq (@Tpoint Tn) P C)) (_ : @Per Tn P Q A) (_ : @Lt Tn A B P Q), @Obtuse Tn A B C *)
  intros A B C D P Q HSac HP HQ HAQ HBP HPC HPerQ Hlt.
(* Goal: @Obtuse Tn A B C *)
  assert(HSac' := HSac).
(* Goal: @Obtuse Tn A B C *)
  destruct HSac'.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @Obtuse Tn A B C *)
  assert(HNCol1 : ~ Col A D B) by (apply (one_side_not_col123 _ _ _ C); auto).
(* Goal: @Obtuse Tn A B C *)
  assert(HNCol2 : ~ Col A B C) by (apply (per2_os__ncol123 _ _ _ D); auto).
(* Goal: @Obtuse Tn A B C *)
  assert(OS A Q B P) by (apply (col_one_side _ D); Col; apply (l9_17 _ _ C); auto).
(* Goal: @Obtuse Tn A B C *)
  assert(HNCol3 : ~ Col A Q P) by (apply (one_side_not_col123 _ _ _ B); Side).
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @Obtuse Tn A B C *)
  assert(Q <> D).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { intro.
(* Goal: False *)
    subst Q.
(* Goal: False *)
    assert(Haux : ~ Col B C D) by (apply (per2_os__ncol234 A); auto).
(* Goal: False *)
    assert(Col C P D).
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
      apply cop_per2__col with A; Perp.
(* Goal: @Coplanar Tn A C R D *)
(* Goal: False *)
      apply coplanar_perm_3, col_cop__cop with B; Col; Cop.
(* Goal: False *)
    apply Haux; ColR.
  }
(* Goal: @Obtuse Tn A B C *)
  assert(OS D Q C P) by (apply (col_one_side _ A); Col; apply (l9_17 _ _ B); Side; Between).
(* Goal: @Obtuse Tn B C A *)
  apply nsams__obtuse; auto.
(* Goal: not (@SAMS Tn D E F B C A) *)
  intro HIsi.
(* Goal: False *)
  assert(HSuma := ex_suma A B C A B C).
(* Goal: False *)
  destruct HSuma as [R [S [T HSuma]]]; auto.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: False *)
  apply (nlta R S T).
(* Goal: @LtA Tn R S T R S T *)
  apply (lea123456_lta__lta _ _ _ B P C).
(* Goal: @LeA Tn R S T B P C *)
(* Goal: @LtA Tn B P C R S T *)
  apply l11_31_2; auto.
(* Goal: @LtA Tn B P C R S T *)
  apply (sams_lta2_suma2__lta B P Q Q P C _ _ _ A B C A B C); auto.
  - apply (conga_preserves_lta B P Q A B P); try (apply conga_refl); auto.
(* Goal: @Out Tn S R I *)
      apply (out_conga A B P A B P); try (apply out_trivial); CongA; apply bet_out; auto.
(* Goal: @LtA Tn B P Q A B P *)
    apply lt_os_per2__lta; auto.
(* Goal: @Per Tn B A S *)
(* Goal: @Per Tn A S I *)
(* Goal: @OS Tn A S B I *)
    apply (per_col _ _ D); Col.
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
    Perp.

  - apply (conga_preserves_lta Q P C P C D); try (apply conga_refl); auto.
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { apply sac__conga in HSac.
(* Goal: @CongA Tn P C D A B C *)
      apply (out_conga B C D A B C); try (apply out_trivial); CongA.
(* Goal: @Out Tn C B C' *)
      apply l6_6; apply bet_out; Between.
    }
(* Goal: @LtA Tn Q P C P C D *)
    apply lt4321_os_per2__lta; Side.
(* Goal: @Per Tn C D S *)
(* Goal: @Per Tn D S I *)
(* Goal: @Cong Tn D C I S *)
(* Goal: @OS Tn D S C I *)
    apply (per_col _ _ A); Perp; Col.
(* Goal: @Per Tn N H G *)
    apply (l8_3 A); Col.
(* Goal: @Lt Tn D C P Q *)
    apply (cong2_lt__lt A B P Q); Cong.

  - exists C.
(* Goal: and (@CongA Tn Q P C Q P C) (and (not (@OS Tn P Q B C)) (and (@Coplanar Tn B P Q C) (@CongA Tn B P C B P C))) *)
    repeat (split; CongA); [|exists C; left; split; Col].
(* Goal: not (@OS Tn C M A B) *)
    apply l9_9.
(* Goal: @TS Tn P Q B C *)
    assert(HNCol4 : ~ Col C P Q).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { apply (per2_os__ncol234 D); auto.
(* Goal: @Per Tn C D S *)
(* Goal: @Per Tn D S I *)
(* Goal: @Cong Tn D C I S *)
(* Goal: @OS Tn D S C I *)
      apply (per_col _ _ A); Perp; Col.
(* Goal: @Per Tn D Q P *)
      apply (l8_3 A); Perp; Col.
    }
(* Goal: @TS Tn P Q B C *)
    repeat split; Col.
(* Goal: not (@Col Tn B P Q) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T P Q) (@Bet Tn B T C)) *)
      intro; apply HNCol4; ColR.
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T P Q) (@Bet Tn B T C)) *)
    exists P; Col.
Qed.

Lemma t22_7__cong : forall A B C D P Q,
  Saccheri A B C D ->
  Bet B P C -> Bet A Q D ->
  A <> Q -> B <> P -> P <> C ->
  Per P Q A -> Per A B C ->
  Cong P Q A B.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Bet Tn B P C) (_ : @Bet Tn A Q D) (_ : not (@eq (@Tpoint Tn) A Q)) (_ : not (@eq (@Tpoint Tn) B P)) (_ : not (@eq (@Tpoint Tn) P C)) (_ : @Per Tn P Q A) (_ : @Per Tn A B C), @Cong Tn P Q A B *)
  intros A B C D P Q HSac HP HQ HAQ HBP HPC HPerQ HPer.
(* Goal: @LtA Tn B D C A B D *)
  assert(Hdiff := sac_distincts A B C D HSac).
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @Cong Tn P Q A B *)
  elim(cong_dec P Q A B); auto.
(* Goal: forall _ : @Obtuse Tn A C B, hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intro.
(* Goal: hypothesis_of_obtuse_saccheri_quadrilaterals *)
  exfalso.
(* Goal: False *)
  apply (nlta A B C).
(* Goal: @LtA Tn A B C A B C *)
  elim(le_cases P Q A B).
  - intro.
(* Goal: @LtA Tn P Q R B C D *)
(* Goal: @SAMS Tn B C A C A B *)
(* Goal: @SumA Tn B C A A C D B C D *)
    apply acute_per__lta; auto.
(* Goal: @Acute Tn A B C *)
    apply (t22_7__acute _ _ _ D P Q); auto.
(* Goal: and (@SumA Tn C A B A B C D E F) (@SumA Tn D E F B C A D E D') *)
    split; auto.

  - intro.
(* Goal: @LtA Tn B C D P Q R *)
(* Goal: @SAMS Tn B C A A C D *)
(* Goal: @SumA Tn B C A A C D B C D *)
    apply obtuse_per__lta; auto.
(* Goal: @Obtuse Tn A B C *)
    apply (t22_7__obtuse _ _ _ D P Q); auto.
(* Goal: @Lt Tn A B R S *)
    split; Cong.
Qed.

Lemma t22_7__lt5612 : forall A B C D P Q,
  Saccheri A B C D ->
  Bet B P C -> Bet A Q D ->
  A <> Q -> B <> P -> P <> C ->
  Per P Q A -> Acute A B C ->
  Lt P Q A B.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Bet Tn B P C) (_ : @Bet Tn A Q D) (_ : not (@eq (@Tpoint Tn) A Q)) (_ : not (@eq (@Tpoint Tn) B P)) (_ : not (@eq (@Tpoint Tn) P C)) (_ : @Per Tn P Q A) (_ : @Acute Tn A B C), @Lt Tn P Q A B *)
  intros A B C D P Q HSac HP HQ HAQ HBP HPC HPerQ Hacute.
(* Goal: @LtA Tn B D C A B D *)
  assert(Hdiff := sac_distincts A B C D HSac).
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @Lt Tn A B P Q *)
  elim(cong_dec P Q A B).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { intro.
(* Goal: hypothesis_of_obtuse_saccheri_quadrilaterals *)
    exfalso.
(* Goal: False *)
    apply (nlta A B C).
(* Goal: @LtA Tn P Q R B C D *)
(* Goal: @SAMS Tn B C A C A B *)
(* Goal: @SumA Tn B C A A C D B C D *)
    apply acute_per__lta; auto.
(* Goal: @Per Tn A B C *)
    apply (t22_7__per _ _ _ D P Q); auto.
  }
(* Goal: forall _ : @Obtuse Tn A C B, hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intro.
(* Goal: and (@SumA Tn C A B A B C D E F) (@SumA Tn D E F B C A D E D') *)
  split; auto.
(* Goal: @Le Tn A B P Q *)
  elim(le_cases P Q A B); auto.
(* Goal: forall _ : @Obtuse Tn A C B, hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intro.
(* Goal: hypothesis_of_obtuse_saccheri_quadrilaterals *)
  exfalso.
(* Goal: False *)
  apply (nlta A B C).
(* Goal: @LtA Tn A B C A B C *)
  apply acute_obtuse__lta; auto.
(* Goal: @Obtuse Tn A B C *)
  apply (t22_7__obtuse _ _ _ D P Q); auto.
(* Goal: @Lt Tn A B R S *)
  split; Cong.
Qed.

Lemma t22_7__lt1256 : forall A B C D P Q,
  Saccheri A B C D ->
  Bet B P C -> Bet A Q D ->
  A <> Q -> B <> P -> P <> C ->
  Per P Q A -> Obtuse A B C ->
  Lt A B P Q.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Bet Tn B P C) (_ : @Bet Tn A Q D) (_ : not (@eq (@Tpoint Tn) A Q)) (_ : not (@eq (@Tpoint Tn) B P)) (_ : not (@eq (@Tpoint Tn) P C)) (_ : @Per Tn P Q A) (_ : @Obtuse Tn A B C), @Lt Tn A B P Q *)
  intros A B C D P Q HSac HP HQ HAQ HBP HPC HPerQ Hobtuse.
(* Goal: @LtA Tn B D C A B D *)
  assert(Hdiff := sac_distincts A B C D HSac).
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @Lt Tn A B P Q *)
  elim(cong_dec P Q A B).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { intro.
(* Goal: hypothesis_of_obtuse_saccheri_quadrilaterals *)
    exfalso.
(* Goal: False *)
    apply (nlta A B C).
(* Goal: @LtA Tn B C D P Q R *)
(* Goal: @SAMS Tn B C A A C D *)
(* Goal: @SumA Tn B C A A C D B C D *)
    apply obtuse_per__lta; auto.
(* Goal: @Per Tn A B C *)
    apply (t22_7__per _ _ _ D P Q); auto.
  }
(* Goal: forall _ : @Obtuse Tn A C B, hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intro.
(* Goal: @Lt Tn A B R S *)
  split; Cong.
(* Goal: @Le Tn A B P Q *)
  elim(le_cases P Q A B); auto.
(* Goal: forall _ : @Obtuse Tn A C B, hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intro.
(* Goal: hypothesis_of_obtuse_saccheri_quadrilaterals *)
  exfalso.
(* Goal: False *)
  apply (nlta A B C).
(* Goal: @LtA Tn A B C A B C *)
  apply acute_obtuse__lta; auto.
(* Goal: @Acute Tn A B C *)
  apply (t22_7__acute _ _ _ D P Q); auto.
(* Goal: and (@SumA Tn C A B A B C D E F) (@SumA Tn D E F B C A D E D') *)
  split; auto.
Qed.


Lemma t22_8__per : forall A B C D R S,
  Saccheri A B C D ->
  Bet B C R -> Bet A D S ->
  C <> R ->
  Per A S R ->
  Cong R S A B ->
  Per A B C.
Proof.
(* Goal: forall (A B C D R S : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Bet Tn B C R) (_ : @Bet Tn A D S) (_ : not (@eq (@Tpoint Tn) C R)) (_ : @Per Tn A S R) (_ : @Cong Tn R S A B), @Per Tn A B C *)
  intros A B C D R S HSac HR HS HCR HPer HCong.
(* Goal: @LtA Tn B D C A B D *)
  assert(Hdiff := sac_distincts A B C D HSac).
(* Goal: @Obtuse Tn A B C *)
  assert(HSac' := HSac).
(* Goal: @Obtuse Tn A B C *)
  unfold Saccheri in HSac'.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @Obtuse Tn A B C *)
  assert(A <> S) by (intro; treat_equalities; auto).
(* Goal: @Obtuse Tn A B C *)
  assert(B <> R) by (intro; treat_equalities; auto).
(* Goal: @Per Tn A B C *)
  assert(HSac' : Saccheri A B R S).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { repeat split; Cong.
(* Goal: @Per Tn B A S *)
(* Goal: @Per Tn A S I *)
(* Goal: @OS Tn A S B I *)
    apply (per_col _ _ D); Col.
(* Goal: @OS Tn A S B R *)
    apply (col_one_side _ D); Col.
(* Goal: @OS Tn K H C D *)
    apply l12_6.
(* Goal: @Par_strict Tn A D B R *)
    apply (par_strict_col_par_strict _ _ _ C); Col.
(* Goal: @Par_strict Tn A D B C *)
    apply sac__par_strict1423; auto.
  }
(* Goal: @Per Tn A S I *)
(* Goal: @OS Tn A S B I *)
  apply (per_col _ _ R); Col.
  apply (t22_7__per _ _ _  S C D); Perp; Cong.
Qed.

Lemma t22_8__acute : forall A B C D R S,
  Saccheri A B C D ->
  Bet B C R -> Bet A D S ->
  C <> R ->
  Per A S R ->
  Lt A B R S ->
  Acute A B C.
Proof.
(* Goal: forall (A B C D R S : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Bet Tn B C R) (_ : @Bet Tn A D S) (_ : not (@eq (@Tpoint Tn) C R)) (_ : @Per Tn A S R) (_ : @Lt Tn R S A B), @Obtuse Tn A B C *)
  intros A B C D R S HSac HR HS HCR HPer Hlt.
(* Goal: @LtA Tn B D C A B D *)
  assert(Hdiff := sac_distincts A B C D HSac).
(* Goal: @Obtuse Tn A B C *)
  assert(HSac' := HSac).
(* Goal: @Obtuse Tn A B C *)
  unfold Saccheri in HSac'.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @Acute Tn A B C *)
  assert(R <> S) by (intro; subst S; destruct Hlt; assert(A = B); auto; apply (le_zero _ _ R); auto).
(* Goal: @Obtuse Tn A B C *)
  assert(A <> S) by (intro; treat_equalities; auto).
(* Goal: @Obtuse Tn A B C *)
  assert(B <> R) by (intro; treat_equalities; auto).
(* Goal: @Acute Tn A B C *)
  assert(HNCol1 : ~ Col A S R) by (apply per_not_col; auto).
(* Goal: @Obtuse Tn A B C *)
  assert(D <> S).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { intro.
(* Goal: False *)
    subst S.
(* Goal: False *)
    assert(Haux : ~ Col B C D) by (apply (per2_os__ncol234 A); auto).
(* Goal: False *)
    assert(Col C R D).
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
      apply cop_per2__col with A; Perp.
(* Goal: @Coplanar Tn A C R D *)
(* Goal: False *)
      apply coplanar_perm_3, col_cop__cop with B; Col; Cop.
(* Goal: False *)
    apply Haux; ColR.
  }
(* Goal: @Acute Tn A B C *)
  assert(HJ := Hlt).
(* Goal: @Acute Tn A B C *)
  apply lt_right_comm in HJ.
(* Goal: @Acute Tn A B C *)
  destruct HJ as [[J []] _].
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @Acute Tn A B C *)
  assert(J <> R) by (intro; subst J; destruct Hlt; Cong).
(* Goal: @Obtuse Tn A B C *)
  assert(CongA A B C B C D) by (apply sac__conga; auto).
(* Goal: @Acute Tn A B C *)
  apply (acute_lea_acute _ _ _ B C D); Lea.
(* Goal: @Acute Tn B C D *)
  apply (acute_chara _ _ _ R); auto.
(* Goal: @LtA Tn B C D R C D *)
  assert(HSac1 : Saccheri A B J S).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { repeat split; Cong.
(* Goal: @Per Tn B A S *)
(* Goal: @Per Tn A S I *)
(* Goal: @OS Tn A S B I *)
    apply (per_col _ _ D); Col.
(* Goal: @Per Tn A S I *)
(* Goal: @OS Tn A S B I *)
    apply (per_col _ _ R); Col.
(* Goal: @OS Tn I B S C *)
    apply (one_side_transitivity _ _ _ R).
    - apply (col_one_side _ D); Col.
(* Goal: @OS Tn K H C D *)
      apply l12_6.
(* Goal: @Par_strict Tn A D B R *)
      apply (par_strict_col_par_strict _ _ _ C); Col.
(* Goal: @Par_strict Tn A D B C *)
      apply sac__par_strict1423; auto.
    - apply invert_one_side, out_one_side; Col.
(* Goal: @Out Tn B R C *)
      apply l6_6, bet_out; auto.
  }
(* Goal: @LtA Tn B C D R C D *)
  assert(HSac2 : Saccheri D C J S).
(* Goal: @SAMS Tn B C A A C D *)
  { repeat split; auto.
(* Goal: @Per Tn C D S *)
(* Goal: @Per Tn D S I *)
(* Goal: @Cong Tn D C I S *)
(* Goal: @OS Tn D S C I *)
    apply (per_col _ _ A); Perp; Col.
(* Goal: @Per Tn N H G *)
    apply (per_col _ _ R); Col; apply (l8_3 A); Col.
(* Goal: @Cong Tn D C I S *)
(* Goal: @OS Tn D S C I *)
    apply (cong_transitivity _ _ A B); Cong.
(* Goal: @OS Tn I B S C *)
    apply (one_side_transitivity _ _ _ R).
    - apply (col_one_side _ A); Col.
(* Goal: @OS Tn D A C R *)
      apply l12_6, (par_strict_col_par_strict _ _ _ B); Col.
(* Goal: @Par_strict Tn D A C B *)
      apply par_strict_comm, sac__par_strict1423; auto.
    - apply invert_one_side, out_one_side.
(* Goal: or (not (@Col Tn S D R)) (not (@Col Tn S D I)) *)
(* Goal: @Out Tn S R I *)
        left; intro; apply HNCol1; ColR.
(* Goal: @Out Tn B R C *)
      apply l6_6, bet_out; auto.
  }
(* Goal: @LtA Tn B C D R C D *)
  assert(CongA A B J B J S) by (apply sac__conga; auto).
(* Goal: @LtA Tn B C D R C D *)
  assert(CongA D C J C J S) by (apply sac__conga; auto).
(* Goal: @LtA Tn B C D R C D *)
  assert(HNCol2 : ~ Col B J S) by (apply (sac__ncol234 A); auto).
(* Goal: @LtA Tn B C D R C D *)
  assert(HNCol3 : ~ Col B J R) by (intro; apply HNCol2; ColR).
(* Goal: @LtA Tn B C D R C D *)
  assert(HNCol4 : ~ Col B J C) by (intro; apply HNCol3; ColR).
(* Goal: @LtA Tn B C D R C D *)
  assert(HNCol5 : ~ Col D C J) by (apply (sac__ncol123 _ _ _ S); auto).
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @LtA Tn B C D R C D *)
  assert(TS C J D R).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { apply (l9_8_2 _ _ S).
(* Goal: @TS Tn C J S R *)
(* Goal: @OS Tn C J S D *)
      repeat split; auto; try (intro; apply HNCol2; ColR); exists J; Col.
(* Goal: @OS Tn C J S D *)
    assert(HPars := sac__par_strict1423 D C J S HSac2).
(* Goal: @OS Tn M N C D *)
(* Goal: @OS Tn M N D K *)
    apply l12_6; Par.
  }
(* Goal: @LtA Tn B C D R C D *)
  apply (sams_lta2_suma2__lta A B J J B C _ _ _ D C J J C R).
  - assert(OS S R C B).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { apply invert_one_side.
(* Goal: @OS Tn I B S R *)
      apply out_one_side.
(* Goal: False *)
      right; intro; apply HNCol2; ColR.
(* Goal: @Out Tn C B C' *)
      apply bet_out; Between.
    }
(* Goal: @LtA Tn A B J D C J *)
    apply (conga_preserves_lta S J B S J C); CongA.
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
    split.
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { exists B.
(* Goal: and (@CongA Tn A' A B A' A B) (and (not (@OS Tn A A' C B)) (and (not (@TS Tn C A A' B)) (@Coplanar Tn C A A' B))) *)
      split; CongA.
(* Goal: @InAngle Tn B S J C *)
      apply os_ts__inangle.
      - apply l9_2, (l9_8_2 _ _ R).
(* Goal: @TS Tn J B R S *)
(* Goal: @OS Tn J B R C *)
          repeat split; Col; exists J; Col; Between.
(* Goal: @OS Tn I B R C *)
        apply invert_one_side, out_one_side; Col.
(* Goal: @Out Tn B R C *)
        apply l6_6, bet_out; auto.
      - apply invert_one_side, (col_one_side _ R); Col.
    }
(* Goal: not (@CongA Tn S I C S I B) *)
    intro Habs.
(* Goal: False *)
    apply conga_cop__or_out_ts in Habs; [|exists R; left; split; Col].
(* Goal: False *)
    destruct Habs.
(* Goal: False *)
(* Goal: False *)
      assert_cols; Col.
(* Goal: False *)
    assert(~ TS S J B C); auto.
(* Goal: not (@TS Tn I C R D) *)
    apply l9_9_bis.
(* Goal: @OS Tn S I C B *)
    apply (col_one_side _ R); Col; Side.

  - apply (conga_preserves_lta C B J J C R); try (apply conga_refl); CongA.
(* Goal: @LtA Tn C B J J C R *)
    assert (HInter := l11_41 C B J R).
(* Goal: not (@SAMS Tn D E F B C A) *)
    destruct HInter; Col.

(* Goal: @SAMS Tn B C A A C D *)
  - repeat split; auto.
(* Goal: or (@Out Tn C J R) (not (@Bet Tn D C J)) *)
(* Goal: @ex (@Tpoint Tn) (fun J0 : @Tpoint Tn => and (@CongA Tn J C J0 J C R) (and (not (@OS Tn C J D J0)) (and (not (@TS Tn D C J J0)) (@Coplanar Tn D C J J0)))) *)
    right; intro; apply HNCol5; Col.
(* Goal: @SumA Tn D C J J C R R C D *)
    exists R.
(* Goal: and (@CongA Tn J C R J C R) (and (not (@OS Tn C J D R)) (and (not (@TS Tn D C J R)) (@Coplanar Tn D C J R))) *)
    split; CongA; repeat split; Cop.
(* Goal: not (@OS Tn C R I D) *)
      apply l9_9; auto.
(* Goal: not (@TS Tn I C R D) *)
    apply l9_9_bis.
(* Goal: @OS Tn K H C D *)
    apply l12_6.
(* Goal: @Par_strict Tn D C J R *)
    apply (par_not_col_strict _ _ _ _ J); Col.
(* Goal: @Par Tn D C J R *)
    apply (par_col_par _ _ _ S); Col.
(* Goal: @Par Tn D C J S *)
    apply sac__par1234, HSac2.

  - exists C.
(* Goal: and (@CongA Tn C B A B C D) (and (not (@OS Tn B C I A)) (and (@Coplanar Tn I B C A) (@CongA Tn I B A A B I))) *)
    repeat (split; CongA).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { apply l9_9.
      apply (l9_8_2 _ _ S);
      [|apply l12_6; assert(HPars := sac__par_strict1423 A B J S HSac1); Par].
(* Goal: @TS Tn M C L H *)
    apply l9_2.
(* Goal: @TS Tn B J C S *)
    apply (l9_8_2 _ _ R).
(* Goal: and (@Col Tn M C M) (@Bet Tn A M B) *)
      repeat split; Col; exists J; split; Col; Between.
(* Goal: @OS Tn B J R C *)
    apply out_one_side; Col.
(* Goal: @Out Tn B R C *)
    apply l6_6, bet_out; auto.
    }
(* Goal: @Coplanar Tn A B J C *)
    apply coplanar_trans_1 with S.
(* Goal: not (@Col Tn S A B) *)
(* Goal: @Coplanar Tn S A B J *)
(* Goal: @Coplanar Tn S A B C *)
      apply per_not_col; auto; apply l8_2, per_col with D; Col.
(* Goal: @Coplanar Tn S B A I *)
(* Goal: @Coplanar Tn S B A C *)
      apply sac__coplanar in HSac1; Cop.
(* Goal: @Coplanar Tn S A B C *)
    apply coplanar_perm_22, col_cop__cop with D; Col; Cop.
  - exists R.
(* Goal: and (@CongA Tn R C D R C D) (and (not (@OS Tn C R I D)) (and (@Coplanar Tn I C R D) (@CongA Tn I C D D C I))) *)
    repeat (split; CongA); Cop.
(* Goal: not (@OS Tn C R I D) *)
    apply l9_9; auto.
Qed.

Lemma t22_8__obtuse : forall A B C D R S,
  Saccheri A B C D ->
  Bet B C R -> Bet A D S ->
  C <> R ->
  Per A S R ->
  Lt R S A B ->
  Obtuse A B C.
Proof.
(* Goal: forall (A B C D R S : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Bet Tn B C R) (_ : @Bet Tn A D S) (_ : not (@eq (@Tpoint Tn) C R)) (_ : @Per Tn A S R) (_ : @Lt Tn R S A B), @Obtuse Tn A B C *)
  intros A B C D R S HSac HR HS HCR HPer Hlt.
(* Goal: @LtA Tn B D C A B D *)
  assert(Hdiff := sac_distincts A B C D HSac).
(* Goal: @Obtuse Tn A B C *)
  assert(HSac' := HSac).
(* Goal: @Obtuse Tn A B C *)
  unfold Saccheri in HSac'.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @Obtuse Tn A B C *)
  assert(A <> S) by (intro; treat_equalities; auto).
(* Goal: @Obtuse Tn A B C *)
  assert(B <> R) by (intro; treat_equalities; auto).
(* Goal: @Obtuse Tn A B C *)
  assert(D <> S).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { intro.
(* Goal: False *)
    subst S.
(* Goal: False *)
    assert(Haux : ~ Col B C D) by (apply (per2_os__ncol234 A); auto).
(* Goal: False *)
    assert(Col C R D).
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
      apply cop_per2__col with A; Perp.
(* Goal: @Coplanar Tn A C R D *)
(* Goal: False *)
      apply coplanar_perm_3, col_cop__cop with B; Col; Cop.
(* Goal: False *)
    apply Haux; ColR.
  }
(* Goal: @Obtuse Tn A B C *)
  assert(HPars := sac__par_strict1423 A B C D HSac).
(* Goal: @Obtuse Tn A B C *)
  assert(OS A S B R).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { apply (col_one_side _ D); Col.
(* Goal: @OS Tn K H C D *)
    apply l12_6.
(* Goal: @Par_strict Tn A D B R *)
    apply (par_strict_col_par_strict _ _ _ C); Col.
  }
(* Goal: @Obtuse Tn A B C *)
  assert(HNCol1 : ~ Col A S R) by (apply (one_side_not_col123 _ _ _ B); Side).
(* Goal: @Obtuse Tn A B C *)
  assert(HI := l5_5_1 S R A B).
(* Goal: @Obtuse Tn A B C *)
  destruct HI as [I []].
(* Goal: @Le Tn S R A B *)
(* Goal: @Obtuse Tn A B C *)
    destruct Hlt; Le.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @Obtuse Tn A B C *)
  assert(R <> I) by (intro; subst I; destruct Hlt; Cong).
(* Goal: @Obtuse Tn A B C *)
  assert(CongA A B C B C D) by (apply sac__conga; auto).
(* Goal: @Obtuse Tn A B C *)
  apply (obtuse_gea_obtuse _ _ _ B C D); [|apply conga__lea; CongA].
(* Goal: @Obtuse Tn B C D *)
  apply (obtuse_chara _ _ _ R); auto.
(* Goal: @LtA Tn R C D B C D *)
  assert(HSac1 : Saccheri A B I S).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { repeat split; Cong.
(* Goal: @Per Tn B A S *)
(* Goal: @Per Tn A S I *)
(* Goal: @OS Tn A S B I *)
    apply (per_col _ _ D); Col.
(* Goal: @Per Tn A S I *)
(* Goal: @OS Tn A S B I *)
    apply (per_col _ _ R); Col.
(* Goal: @OS Tn I B S C *)
    apply (one_side_transitivity _ _ _ R).
    - apply (col_one_side _ D); Col.
(* Goal: @OS Tn A D B R *)
      apply l12_6, (par_strict_col_par_strict _ _ _ C); Col.
    - apply invert_one_side, out_one_side; Col.
(* Goal: @Out Tn S R I *)
      apply bet_out; auto.
  }
(* Goal: @LtA Tn R C D B C D *)
  assert(HSac2 : Saccheri D C I S).
(* Goal: @SAMS Tn B C A A C D *)
  { repeat split; auto.
(* Goal: @Per Tn C D S *)
(* Goal: @Per Tn D S I *)
(* Goal: @Cong Tn D C I S *)
(* Goal: @OS Tn D S C I *)
    apply (per_col _ _ A); Perp; Col.
(* Goal: @Per Tn N H G *)
    apply (per_col _ _ R); Col; apply (l8_3 A); Col.
(* Goal: @Cong Tn D C I S *)
(* Goal: @OS Tn D S C I *)
    apply (cong_transitivity _ _ A B); Cong.
(* Goal: @OS Tn I B S C *)
    apply (one_side_transitivity _ _ _ R).
    - apply (col_one_side _ A); Col.
(* Goal: @OS Tn D A C R *)
      apply l12_6, (par_strict_col_par_strict _ _ _ B); Col; Par.
    - apply invert_one_side, out_one_side.
(* Goal: or (not (@Col Tn S D R)) (not (@Col Tn S D I)) *)
(* Goal: @Out Tn S R I *)
        left; intro; apply HNCol1; ColR.
(* Goal: @Out Tn S R I *)
      apply bet_out; auto.
  }
(* Goal: @LtA Tn R C D B C D *)
  assert(CongA A B I B I S) by (apply sac__conga; auto).
(* Goal: @LtA Tn R C D B C D *)
  assert(CongA D C I C I S) by (apply sac__conga; auto).
(* Goal: @LtA Tn R C D B C D *)
  assert(HNCol2 : ~ Col C I S) by (apply (sac__ncol234 D); auto).
(* Goal: @LtA Tn R C D B C D *)
  assert(HNCol3 : ~ Col C I R) by (intro; apply HNCol2; ColR).
(* Goal: @LtA Tn R C D B C D *)
  assert(HNCol4 : ~ Col C I B) by (intro; apply HNCol3; ColR).
(* Goal: @LtA Tn R C D B C D *)
  assert(HNCol5 : ~ Col D C I) by (apply (sac__ncol123 _ _ _ S); auto).
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @LtA Tn R C D B C D *)
  assert(TS C R I D).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { apply l9_2.
(* Goal: @TS Tn B C A I *)
    apply (l9_8_2 _ _ S).
(* Goal: @TS Tn C R S I *)
(* Goal: @OS Tn C R S D *)
      repeat split; auto; try (intro; apply HNCol2; ColR); exists R; Col.
(* Goal: @OS Tn C R S D *)
    apply one_side_symmetry.
(* Goal: @OS Tn C R D S *)
    apply (col_one_side _ B); Col.
(* Goal: @OS Tn K H C D *)
    apply l12_6.
(* Goal: @Par_strict Tn C B D S *)
    apply (par_strict_col_par_strict _ _ _ A); Col; Par.
  }
(* Goal: @LtA Tn R C D B C D *)
  apply(sams_lta2_suma2__lta456 I C R _ _ _ D C I I B C _ _ _ A B I).
  - apply lta_left_comm.
(* Goal: @LtA Tn C B I I C R *)
    assert (HInter := l11_41 C B I R).
(* Goal: not (@SAMS Tn D E F B C A) *)
    destruct HInter; Col.

  - assert(OS R S C B).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { apply out_one_side.
(* Goal: False *)
        right; intro; apply HNCol2; ColR.
(* Goal: @Out Tn C B C' *)
      apply bet_out; Between.
    }
(* Goal: @LtA Tn D C I A B I *)
    apply (conga_preserves_lta S I C S I B); CongA.
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
    split.
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { exists C.
(* Goal: and (@CongA Tn A' A B A' A B) (and (not (@OS Tn A A' C B)) (and (not (@TS Tn C A A' B)) (@Coplanar Tn C A A' B))) *)
      split; CongA.
(* Goal: @InAngle Tn C S I B *)
      apply os2__inangle.
(* Goal: @OS Tn I S B C *)
(* Goal: @OS Tn I B S C *)
        apply invert_one_side, (col_one_side _ R); Col; Side.
(* Goal: @OS Tn I B S C *)
      apply (one_side_transitivity _ _ _ R).
(* Goal: @OS Tn I B S R *)
      - apply out_one_side.
(* Goal: or (not (@Col Tn I B S)) (not (@Col Tn I B R)) *)
(* Goal: @Out Tn I S R *)
          right; intro; apply HNCol3; ColR.
(* Goal: @Out Tn C B M *)
        apply l6_6, bet_out; Between.
      - apply invert_one_side, out_one_side; Col.
(* Goal: @Out Tn B R C *)
        apply l6_6, bet_out; auto.
    }
(* Goal: not (@CongA Tn S I C S I B) *)
    intro Habs.
(* Goal: False *)
    apply conga_cop__or_out_ts in Habs; [|exists R; left; split; Col].
(* Goal: False *)
    destruct Habs.
(* Goal: False *)
(* Goal: False *)
      assert_cols; Col.
(* Goal: False *)
    assert(~ TS S I C B); auto.
(* Goal: not (@TS Tn I C R D) *)
    apply l9_9_bis.
(* Goal: @OS Tn S I C B *)
    apply (col_one_side _ R); Col; Side.

(* Goal: @SAMS Tn B C A A C D *)
  - repeat split; auto.
(* Goal: not (@Col Tn B P Q) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T P Q) (@Bet Tn B T C)) *)
    right; intro; apply HNCol4; ColR.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Per Tn B C C') (@GtA Tn P Q R B C C')) *)
    exists D.
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
    split; CongA; split.
(* Goal: not (@OS Tn C R I D) *)
      apply l9_9; auto.
(* Goal: and (not (@TS Tn I C R D)) (@Coplanar Tn I C R D) *)
    split; Cop.
(* Goal: not (@TS Tn I C R D) *)
    apply l9_9_bis.
(* Goal: @OS Tn I C R D *)
    apply (one_side_transitivity _ _ _ S).
(* Goal: @Out Tn C B C' *)
    apply out_one_side; Col; apply bet_out; Between.
(* Goal: @OS Tn K H C D *)
    apply l12_6.
(* Goal: @Par_strict Tn I C S D *)
    assert(Haux := sac__par_strict1423 D C I S HSac2); Par.

  - exists D.
(* Goal: and (@CongA Tn R C D R C D) (and (not (@OS Tn C R I D)) (and (@Coplanar Tn I C R D) (@CongA Tn I C D D C I))) *)
    repeat (split; CongA); Cop.
(* Goal: not (@OS Tn C R I D) *)
    apply l9_9; auto.

  - exists A.
(* Goal: and (@CongA Tn C B A B C D) (and (not (@OS Tn B C I A)) (and (@Coplanar Tn I B C A) (@CongA Tn I B A A B I))) *)
    repeat (split; CongA).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { apply l9_9.
(* Goal: @TS Tn M C L H *)
      apply l9_2.
(* Goal: @TS Tn B C A I *)
      apply (l9_8_2 _ _ S).
(* Goal: and (@Col Tn I A D) (@Bet Tn B I C) *)
        repeat split; Col; try (intro; apply HNCol2; ColR); exists R; split; Col.
(* Goal: @OS Tn B C S A *)
      apply one_side_symmetry, l12_6.
(* Goal: @Par_strict Tn B C A S *)
      apply (par_strict_col_par_strict _ _ _ D); Col; Par.
    }
(* Goal: @Coplanar Tn I B C A *)
    assert (HNCol6 : ~ Col B A D) by (apply per_not_col; auto).
(* Goal: @Coplanar Tn I B C A *)
    apply coplanar_perm_13, coplanar_trans_1 with S.
(* Goal: not (@Col Tn S B A) *)
(* Goal: @Coplanar Tn S B A I *)
(* Goal: @Coplanar Tn S B A C *)
      intro; apply HNCol6; ColR.
(* Goal: @Coplanar Tn S B A I *)
(* Goal: @Coplanar Tn S B A C *)
      apply sac__coplanar in HSac1; Cop.
(* Goal: @Coplanar Tn S B A C *)
    apply coplanar_perm_19, col_cop__cop with D; Col; Cop.
Qed.

Lemma t22_8__cong : forall A B C D R S,
  Saccheri A B C D -> Bet B C R -> Bet A D S ->
  C <> R -> Per A S R -> Per A B C -> Cong R S A B.
Proof.
(* Goal: forall (A B C D R S : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Bet Tn B C R) (_ : @Bet Tn A D S) (_ : not (@eq (@Tpoint Tn) C R)) (_ : @Per Tn A S R) (_ : @Obtuse Tn A B C), @Lt Tn R S A B *)
  intros A B C D R S HSac.
(* Goal: forall (_ : @Bet Tn B C R) (_ : @Bet Tn A D S) (_ : not (@eq (@Tpoint Tn) C R)) (_ : @Per Tn A S R) (_ : @Obtuse Tn A B C), @Lt Tn R S A B *)
  intros.
(* Goal: @Cong Tn R S A B *)
  elim(cong_dec R S A B); auto.
(* Goal: forall _ : @Obtuse Tn A C B, hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intro.
(* Goal: @LtA Tn B D C A B D *)
  assert(Hdiff := sac_distincts A B C D HSac).
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: hypothesis_of_obtuse_saccheri_quadrilaterals *)
  exfalso.
(* Goal: False *)
  apply (nlta A B C).
(* Goal: @Lt Tn R S A B *)
  destruct(le_cases R S A B).
  - apply obtuse_per__lta; auto.
(* Goal: @Obtuse Tn A B C *)
    apply (t22_8__obtuse _ _ _ D R S); auto.
(* Goal: and (@SumA Tn C A B A B C D E F) (@SumA Tn D E F B C A D E D') *)
    split; auto.

  - apply acute_per__lta; auto.
(* Goal: @Acute Tn A B C *)
    apply (t22_8__acute _ _ _ D R S); auto.
(* Goal: @Lt Tn A B R S *)
    split; Cong.
Qed.

Lemma t22_8__lt1256 : forall A B C D R S,
  Saccheri A B C D ->
  Bet B C R -> Bet A D S ->
  C <> R ->
  Per A S R -> Acute A B C ->
  Lt A B R S.
Proof.
(* Goal: forall (A B C D R S : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Bet Tn B C R) (_ : @Bet Tn A D S) (_ : not (@eq (@Tpoint Tn) C R)) (_ : @Per Tn A S R) (_ : @Obtuse Tn A B C), @Lt Tn R S A B *)
  intros A B C D R S HSac.
(* Goal: forall (_ : @Bet Tn B C R) (_ : @Bet Tn A D S) (_ : not (@eq (@Tpoint Tn) C R)) (_ : @Per Tn A S R) (_ : @Obtuse Tn A B C), @Lt Tn R S A B *)
  intros.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @Lt Tn R S A B *)
  destruct(cong_dec R S A B).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { exfalso.
(* Goal: False *)
    apply (nlta A B C), acute_per__lta; auto.
(* Goal: @Per Tn A B C *)
    apply (t22_8__per _ _ _ D R S); auto.
  }
(* Goal: @Lt Tn A B R S *)
  destruct(le_cases R S A B); [|split; Cong].
(* Goal: hypothesis_of_obtuse_saccheri_quadrilaterals *)
  exfalso.
(* Goal: False *)
  apply (nlta A B C), acute_obtuse__lta; auto.
(* Goal: @Obtuse Tn A B C *)
  apply (t22_8__obtuse _ _ _ D R S); auto.
(* Goal: and (@SumA Tn C A B A B C D E F) (@SumA Tn D E F B C A D E D') *)
  split; auto.
Qed.

Lemma t22_8__lt5612 : forall A B C D R S,
  Saccheri A B C D ->
  Bet B C R -> Bet A D S ->
  C <> R ->
  Per A S R -> Obtuse A B C ->
  Lt R S A B.
Proof.
(* Goal: forall (A B C D R S : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Bet Tn B C R) (_ : @Bet Tn A D S) (_ : not (@eq (@Tpoint Tn) C R)) (_ : @Per Tn A S R) (_ : @Obtuse Tn A B C), @Lt Tn R S A B *)
  intros A B C D R S HSac.
(* Goal: forall (_ : @Bet Tn B C R) (_ : @Bet Tn A D S) (_ : not (@eq (@Tpoint Tn) C R)) (_ : @Per Tn A S R) (_ : @Obtuse Tn A B C), @Lt Tn R S A B *)
  intros.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @Lt Tn R S A B *)
  destruct(cong_dec R S A B).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { exfalso.
(* Goal: False *)
    apply (nlta A B C).
(* Goal: @LtA Tn B C D P Q R *)
(* Goal: @SAMS Tn B C A A C D *)
(* Goal: @SumA Tn B C A A C D B C D *)
    apply obtuse_per__lta; auto.
(* Goal: @Per Tn A B C *)
    apply (t22_8__per _ _ _ D R S); auto.
  }
(* Goal: @Lt Tn R S A B *)
  destruct(le_cases R S A B).
(* Goal: and (@SumA Tn C A B A B C D E F) (@SumA Tn D E F B C A D E D') *)
    split; auto.
(* Goal: hypothesis_of_obtuse_saccheri_quadrilaterals *)
  exfalso.
(* Goal: False *)
  apply (nlta A B C).
(* Goal: @LtA Tn A B C A B C *)
  apply acute_obtuse__lta; auto.
(* Goal: @Acute Tn A B C *)
  apply (t22_8__acute _ _ _ D R S); auto.
(* Goal: @Lt Tn A B R S *)
  split; Cong.
Qed.


Lemma t22_9__per : forall N M P Q R S,
  Lambert N M P Q -> Lambert N M R S ->
  Bet M P R -> Bet N Q S ->
  (Per S R M <-> Per Q P M).
Proof.
(* Goal: forall (N M P Q R S : @Tpoint Tn) (_ : @Lambert Tn N M P Q) (_ : @Lambert Tn N M R S) (_ : @Bet Tn M P R) (_ : @Bet Tn N Q S), iff (@Obtuse Tn S R M) (@Obtuse Tn Q P M) *)
  intros N M P Q R S HLamP HLamR HR HS.
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  destruct(eq_dec_points P R).
(* Goal: False *)
  { unfold Lambert in *.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
    treat_equalities.
(* Goal: iff (@Acute Tn S P M) (@Acute Tn Q P M) *)
    assert(Q = S); [|subst; split; auto].
(* Goal: @eq (@Tpoint Tn) Q S *)
    apply (l8_18_uniqueness N Q P); Col.
(* Goal: not (@Col Tn M N H) *)
    apply per_not_col; auto.
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
      Perp.
(* Goal: @Perp Tn N Q P S *)
    apply (perp_col _ S); Perp; Col.
  }
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(HP' := symmetric_point_construction P M).
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  destruct HP' as [P' HP'].
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  apply l7_2 in HP'.
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(HQ' := symmetric_point_construction Q N).
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  destruct HQ' as [Q' HQ'].
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  apply l7_2 in HQ'.
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(HR' := symmetric_point_construction R M).
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  destruct HR' as [R' HR'].
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  apply l7_2 in HR'.
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(HS' := symmetric_point_construction S N).
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  destruct HS' as [S' HS'].
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  apply l7_2 in HS'.
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(HSacR := lam6534_mid2__sac S' R' R S M N HLamR HR' HS').
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(HSacP := lam6534_mid2__sac Q' P' P Q M N HLamP HP' HQ').
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(Cong S' R' R S /\ Cong Q' P' P Q) by (unfold Saccheri in *; spliter; split; auto).
(* Goal: False *)
  unfold Lambert in *.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(HCongaR := sac__conga S' R' R S HSacR).
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(HCongaQ := sac__conga Q' P' P Q HSacP).
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(Bet P' P R) by (apply (outer_transitivity_between2 _ M); Between).
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(Bet Q' Q S) by (apply (outer_transitivity_between2 _ N); Between).
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(Bet R' P R) by (apply (between_exchange2 _ M); Between).
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(Bet S' Q S) by (apply (between_exchange2 _ N); Between).
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(Per Q' S R) by (apply (l8_3 N); auto; ColR).
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(Per S' Q P) by (apply (l8_3 N); auto; ColR).
(* Goal: forall _ : @Obtuse Tn A C B, hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split; intro.
  - apply (per_col _ _ P'); Col.
(* Goal: @Per Tn Q P P' *)
    apply (l11_17 Q' P' P); CongA.
(* Goal: @Per Tn Q' P' P *)
    apply (t22_8__per _ _ _ Q R S); auto.
(* Goal: @Cong Tn P Q S' R' *)
    apply cong_symmetry.
(* Goal: @Cong Tn Q' P' R S *)
    apply (cong_transitivity _ _ S' R'); auto.
(* Goal: @Cong Tn Q' P' S' R' *)
    apply (cong_transitivity _ _ P Q); auto.
(* Goal: @Cong Tn P Q S' R' *)
    apply (t22_7__cong _ _ R S); auto; try (intro; treat_equalities; auto).
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
      Perp.
(* Goal: @Per Tn S' R' R *)
    apply (l11_17 S R R'); CongA.
(* Goal: @Per Tn Q P P' *)
    apply (per_col _ _ M); Col.

  - apply (per_col _ _ R'); Col.
(* Goal: @Per Tn S R R' *)
    apply (l11_17 S' R' R); CongA.
(* Goal: @Per Tn S' R' R *)
    apply (t22_7__per _ _ _ S P Q); auto; try (intro; treat_equalities; auto).
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
      Perp.
(* Goal: @Cong Tn P Q S' R' *)
    apply cong_symmetry.
(* Goal: @Cong Tn S' R' P Q *)
    apply (cong_transitivity _ _ Q' P'); auto.
(* Goal: @Cong Tn S' R' Q' P' *)
    apply (cong_transitivity _ _ R S); auto.
(* Goal: @Cong Tn R S Q' P' *)
    apply (t22_8__cong _ _ P Q); auto.
(* Goal: @Per Tn Q' P' P *)
    apply (l11_17 Q P P'); CongA.
(* Goal: @Per Tn Q P P' *)
    apply (per_col _ _ M); Col.
Qed.

Lemma t22_9__acute : forall N M P Q R S,
  Lambert N M P Q -> Lambert N M R S ->
  Bet M P R -> Bet N Q S ->
  (Acute S R M <-> Acute Q P M).
Proof.
(* Goal: forall (N M P Q R S : @Tpoint Tn) (_ : @Lambert Tn N M P Q) (_ : @Lambert Tn N M R S) (_ : @Bet Tn M P R) (_ : @Bet Tn N Q S), iff (@Obtuse Tn S R M) (@Obtuse Tn Q P M) *)
  intros N M P Q R S HLamP HLamR HR HS.
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  destruct(eq_dec_points P R).
(* Goal: False *)
  { unfold Lambert in *.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
    treat_equalities.
(* Goal: iff (@Acute Tn S P M) (@Acute Tn Q P M) *)
    assert(Q = S); [|subst; split; auto].
(* Goal: @eq (@Tpoint Tn) Q S *)
    apply (l8_18_uniqueness N Q P); Col.
(* Goal: not (@Col Tn M N H) *)
    apply per_not_col; auto.
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
      Perp.
(* Goal: @Perp Tn N Q P S *)
    apply (perp_col _ S); Perp; Col.
  }
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(HP' := symmetric_point_construction P M).
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  destruct HP' as [P' HP'].
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  apply l7_2 in HP'.
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(HQ' := symmetric_point_construction Q N).
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  destruct HQ' as [Q' HQ'].
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  apply l7_2 in HQ'.
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(HR' := symmetric_point_construction R M).
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  destruct HR' as [R' HR'].
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  apply l7_2 in HR'.
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(HS' := symmetric_point_construction S N).
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  destruct HS' as [S' HS'].
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  apply l7_2 in HS'.
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(HSacR := lam6534_mid2__sac S' R' R S M N HLamR HR' HS').
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(HSacP := lam6534_mid2__sac Q' P' P Q M N HLamP HP' HQ').
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(Cong S' R' R S /\ Cong Q' P' P Q) by (unfold Saccheri in *; spliter; split; auto).
(* Goal: False *)
  unfold Lambert in *.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(HCongaR := sac__conga S' R' R S HSacR).
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(HCongaQ := sac__conga Q' P' P Q HSacP).
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(Bet P' P R) by (apply (outer_transitivity_between2 _ M); Between).
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(Bet Q' Q S) by (apply (outer_transitivity_between2 _ N); Between).
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(Bet R' P R) by (apply (between_exchange2 _ M); Between).
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(Bet S' Q S) by (apply (between_exchange2 _ N); Between).
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(Per Q' S R) by (apply (l8_3 N); auto; ColR).
(* Goal: iff (@Acute Tn S R M) (@Acute Tn Q P M) *)
  assert(Per S' Q P) by (apply (l8_3 N); auto; ColR).
(* Goal: forall _ : @Obtuse Tn A C B, hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split; intro.
  - apply (acute_conga__acute Q' P' P).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { apply (t22_8__acute _ _ _ Q R S); auto.
(* Goal: @Lt Tn Q' P' R S *)
      apply (cong2_lt__lt P Q S' R'); Cong.
(* Goal: @Lt Tn P Q S' R' *)
      apply (t22_7__lt5612 _ _ R S); Perp; try (intro; treat_equalities; auto).
(* Goal: @Acute Tn S' R' R *)
      apply (acute_conga__acute S R M); auto.
(* Goal: @CongA Tn S R M S' R' R *)
      apply (out_conga S R R' S' R' R); try (apply out_trivial); CongA.
(* Goal: @Out Tn C B C' *)
      apply l6_6; apply bet_out; Between.
    }
(* Goal: @CongA Tn Q' P' P Q P M *)
    apply (out_conga Q' P' P Q P P'); try (apply out_trivial); CongA.
(* Goal: @Out Tn C B C' *)
    apply l6_6; apply bet_out; Between.

  - apply (acute_conga__acute S' R' R).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { apply (t22_7__acute _ _ _ S P Q); Perp; try (intro; treat_equalities; auto).
(* Goal: @Lt Tn P Q S' R' *)
      apply (cong2_lt__lt Q' P' R S); Cong.
(* Goal: @Lt Tn Q' P' R S *)
      apply (t22_8__lt1256 _ _ P Q); auto.
(* Goal: @Acute Tn Q' P' P *)
      apply (acute_conga__acute Q P M); auto.
(* Goal: @CongA Tn Q P M Q' P' P *)
      apply (out_conga Q P P' Q' P' P); try (apply out_trivial); CongA.
(* Goal: @Out Tn C B C' *)
      apply l6_6; apply bet_out; Between.
    }
(* Goal: @CongA Tn S' R' R S R M *)
    apply (out_conga S' R' R S R R'); try (apply out_trivial); CongA.
(* Goal: @Out Tn C B C' *)
    apply l6_6; apply bet_out; Between.
Qed.

Lemma t22_9__obtuse : forall N M P Q R S,
  Lambert N M P Q -> Lambert N M R S ->
  Bet M P R -> Bet N Q S ->
  (Obtuse S R M <-> Obtuse Q P M).
Proof.
(* Goal: forall (N M P Q R S : @Tpoint Tn) (_ : @Lambert Tn N M P Q) (_ : @Lambert Tn N M R S) (_ : @Bet Tn M P R) (_ : @Bet Tn N Q S), iff (@Obtuse Tn S R M) (@Obtuse Tn Q P M) *)
  intros N M P Q R S HLamP HLamR HR HS.
(* Goal: forall _ : @Obtuse Tn A C B, hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split; intro.
  - assert(H' := HLamP).
(* Goal: @Obtuse Tn S R M *)
    unfold Lambert in H'.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: @LeA Tn D E F C A B' *)
    assert_diffs.
(* Goal: @Obtuse Tn Q P M *)
    destruct(angle_partition Q P M) as [|[|]]; auto; exfalso; apply (nlta S R M).
(* Goal: @LtA Tn A B C A B C *)
      apply acute_obtuse__lta; auto.
(* Goal: @Acute Tn S R M *)
(* Goal: @LtA Tn S R M S R M *)
      apply (t22_9__acute N _ P Q); auto.
(* Goal: @LtA Tn B C D P Q R *)
(* Goal: @SAMS Tn B C A A C D *)
(* Goal: @SumA Tn B C A A C D B C D *)
    apply obtuse_per__lta; auto.
(* Goal: @Per Tn S R M *)
    apply (t22_9__per N _ P Q); auto.

  - assert(H' := HLamR).
(* Goal: @Obtuse Tn S R M *)
    unfold Lambert in H'.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: @LeA Tn D E F C A B' *)
    assert_diffs.
(* Goal: @Obtuse Tn S R M *)
    destruct(angle_partition S R M) as [|[|]]; auto; exfalso; apply (nlta Q P M).
(* Goal: @LtA Tn A B C A B C *)
      apply acute_obtuse__lta; auto.
(* Goal: @Acute Tn Q P M *)
(* Goal: @LtA Tn Q P M Q P M *)
      apply (t22_9__acute N _ _ _ R S); auto.
(* Goal: @LtA Tn B C D P Q R *)
(* Goal: @SAMS Tn B C A A C D *)
(* Goal: @SumA Tn B C A A C D B C D *)
    apply obtuse_per__lta; auto.
(* Goal: @Per Tn Q P M *)
    apply (t22_9__per N _ _ _ R S); auto.
Qed.

(** The two following lemmas come from Theorem 22.4 *)

Lemma cong2_lam2__cong : forall N M P Q N' M' P' Q',
  Lambert N M P Q -> Lambert N' M' P' Q' ->
  Cong N Q N' Q' -> Cong P Q P' Q' ->
  Cong N M N' M'.
Proof.
(* Goal: forall (N M P Q N' M' P' Q' : @Tpoint Tn) (_ : @Lambert Tn N M P Q) (_ : @Lambert Tn N' M' P' Q') (_ : @Cong Tn N Q N' Q') (_ : @Cong Tn P Q P' Q'), @CongA Tn M P Q M' P' Q' *)
  intros N M P Q N' M' P' Q' HLam HLam' HCong1 HCong2.
(* Goal: @CongA Tn M P Q M' P' Q' *)
  assert(Par_strict N Q M P) by (apply lam__par_strict1423, HLam).
(* Goal: @CongA Tn M P Q M' P' Q' *)
  assert(Par_strict N M P Q) by (apply lam__par_strict1234, HLam).
(* Goal: @CongA Tn M P Q M' P' Q' *)
  assert(Par_strict N' Q' M' P') by (apply lam__par_strict1423, HLam').
(* Goal: @CongA Tn M P Q M' P' Q' *)
  assert(Par_strict N' M' P' Q') by (apply lam__par_strict1234, HLam').
(* Goal: False *)
  unfold Lambert in *.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @CongA Tn M P Q M' P' Q' *)
  assert(~ Col N M P) by (apply per_not_col; auto).
(* Goal: @CongA Tn M P Q M' P' Q' *)
  assert(~ Col M N Q) by (apply per_not_col; auto).
(* Goal: @CongA Tn M P Q M' P' Q' *)
  assert(~ Col M' N' Q') by (apply per_not_col; auto).
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @CongA Tn M P Q M' P' Q' *)
  assert(HSAS := l11_49 N Q P N' Q' P').
(* Goal: @CongA Tn M P Q M' P' Q' *)
  destruct HSAS as [HCong3 [HConga1 HConga2]]; Cong.
(* Goal: @CongA Tn A D C A' D' C' *)
    apply l11_16; auto.
(* Goal: @CongA Tn M P Q M' P' Q' *)
  assert(CongA M N P M' N' P').
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { apply (l11_22b _ _ _ Q _ _ _ Q').
(* Goal: and (@SumA Tn C A B A B C D E F) (@SumA Tn D E F B C A D E D') *)
    split; Side; split; Side; split; auto.
(* Goal: @CongA Tn A D C A' D' C' *)
    apply l11_16; auto.
  }
(* Goal: @CongA Tn M P Q M' P' Q' *)
  assert(HAAS := l11_50_2 P N M P' N' M').
(* Goal: @CongA Tn M P Q M' P' Q' *)
  destruct HAAS as [HCong4 [HCong5 HCong6]]; Col; Cong.
(* Goal: @CongA Tn A D C A' D' C' *)
    apply l11_16; auto.
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
    CongA.
Qed.

Lemma cong2_lam2__conga : forall N M P Q N' M' P' Q',
  Lambert N M P Q -> Lambert N' M' P' Q' ->
  Cong N Q N' Q' -> Cong P Q P' Q' ->
  CongA M P Q M' P' Q'.
Proof.
(* Goal: forall (N M P Q N' M' P' Q' : @Tpoint Tn) (_ : @Lambert Tn N M P Q) (_ : @Lambert Tn N' M' P' Q') (_ : @Cong Tn N Q N' Q') (_ : @Cong Tn P Q P' Q'), @CongA Tn M P Q M' P' Q' *)
  intros N M P Q N' M' P' Q' HLam HLam' HCong1 HCong2.
(* Goal: @CongA Tn M P Q M' P' Q' *)
  assert(Par_strict N Q M P) by (apply lam__par_strict1423, HLam).
(* Goal: @CongA Tn M P Q M' P' Q' *)
  assert(Par_strict N M P Q) by (apply lam__par_strict1234, HLam).
(* Goal: @CongA Tn M P Q M' P' Q' *)
  assert(Par_strict N' Q' M' P') by (apply lam__par_strict1423, HLam').
(* Goal: @CongA Tn M P Q M' P' Q' *)
  assert(Par_strict N' M' P' Q') by (apply lam__par_strict1234, HLam').
(* Goal: False *)
  unfold Lambert in *.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @CongA Tn M P Q M' P' Q' *)
  assert(~ Col N M P) by (apply per_not_col; auto).
(* Goal: @CongA Tn M P Q M' P' Q' *)
  assert(~ Col M N Q) by (apply per_not_col; auto).
(* Goal: @CongA Tn M P Q M' P' Q' *)
  assert(~ Col M' N' Q') by (apply per_not_col; auto).
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @CongA Tn M P Q M' P' Q' *)
  assert(HSAS := l11_49 N Q P N' Q' P').
(* Goal: @CongA Tn M P Q M' P' Q' *)
  destruct HSAS as [HCong3 [HConga1 HConga2]]; Cong.
(* Goal: @CongA Tn A D C A' D' C' *)
    apply l11_16; auto.
(* Goal: @CongA Tn M P Q M' P' Q' *)
  assert(CongA M N P M' N' P').
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { apply (l11_22b _ _ _ Q _ _ _ Q').
(* Goal: and (@SumA Tn C A B A B C D E F) (@SumA Tn D E F B C A D E D') *)
    split; Side; split; Side; split; auto.
(* Goal: @CongA Tn A D C A' D' C' *)
    apply l11_16; auto.
  }
(* Goal: @CongA Tn M P Q M' P' Q' *)
  assert(HAAS := l11_50_2 P N M P' N' M').
(* Goal: @CongA Tn M P Q M' P' Q' *)
  destruct HAAS as [HCong4 [HCong5 HCong6]]; Col; Cong.
(* Goal: @CongA Tn A D C A' D' C' *)
    apply l11_16; auto.
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
    CongA.
(* Goal: @CongA Tn M P Q M' P' Q' *)
  apply (l11_22a _ _ _ N _ _ _ N').
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split.
(* Goal: @TS Tn P' N' M' Q' *)
(* Goal: and (@CongA Tn M P N M' P' N') (@CongA Tn N P Q N' P' Q') *)
    apply l9_31; Side.
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split.
(* Goal: @TS Tn P' N' M' Q' *)
(* Goal: and (@CongA Tn M P N M' P' N') (@CongA Tn N P Q N' P' Q') *)
    apply l9_31; Side.
(* Goal: and (@CongA Tn A' A B A' A B) (and (not (@OS Tn A A' C B)) (and (not (@TS Tn C A A' B)) (@Coplanar Tn C A A' B))) *)
  split; CongA.
Qed.

Lemma cong2_sac2__cong : forall A B C D A' B' C' D',
  Saccheri A B C D -> Saccheri A' B' C' D' ->
  Cong A B A' B' -> Cong A D A' D' ->
  Cong B C B' C'.
Proof.
(* Goal: forall (A B C D A' B' C' D' : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Saccheri Tn A' B' C' D') (_ : @Cong Tn A B A' B') (_ : @Cong Tn A D A' D'), @Cong Tn B C B' C' *)
  intros A B C D A' B' C' D' HSac HSac' HCongB HCongL.
(* Goal: @LtA Tn B D C A B D *)
  assert(Hdiff := sac_distincts A B C D HSac).
(* Goal: @Obtuse Tn A' B' C' *)
  assert(Hdiff' := sac_distincts A' B' C' D' HSac').
(* Goal: @Cong Tn B C B' C' *)
  unfold Saccheri in *.
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @Cong Tn B C B' C' *)
  destruct (l11_49 B A D B' A' D') as [HCongD [HConga1 HConga2]]; Cong.
(* Goal: @CongA Tn A D C A' D' C' *)
    apply l11_16; auto.
  destruct (l11_49 B D C B' D' C'); Cong;
  [|apply (cong_transitivity _ _ A B); Cong; apply (cong_transitivity _ _ A' B'); Cong].
(* Goal: @CongA Tn B D C B' D' C' *)
  apply (l11_22b _ _ _ A _ _ _ A').
(* Goal: and (@OS Tn D' A' B' C') (and (@CongA Tn B D A B' D' A') (@CongA Tn A D C A' D' C')) *)
  split; Side.
(* Goal: and (@OS Tn D' A' B' C') (and (@CongA Tn B D A B' D' A') (@CongA Tn A D C A' D' C')) *)
  split; Side.
(* Goal: and (@CongA Tn A' A B A' A B) (and (not (@OS Tn A A' C B)) (and (not (@TS Tn C A A' B)) (@Coplanar Tn C A A' B))) *)
  split; CongA.
(* Goal: @CongA Tn A D C A' D' C' *)
  apply l11_16; auto.
Qed.

Lemma sac__perp1214 : forall A B C D, Saccheri A B C D -> Perp A B A D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D), iff (@LtA Tn B D C A B D) (@Obtuse Tn A B C) *)
  intros A B C D HSac.
(* Goal: @LtA Tn B D C A B D *)
  assert (Hdiff := sac_distincts A B C D HSac).
(* Goal: @LtA Tn A C D B A C *)
  unfold Saccheri in HSac; spliter.
(* Goal: @Perp Tn A B A D *)
  apply perp_left_comm, per_perp; auto.
Qed.

Lemma sac__perp3414 : forall A B C D, Saccheri A B C D -> Perp C D A D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D), iff (@LtA Tn B D C A B D) (@Obtuse Tn A B C) *)
  intros A B C D HSac.
(* Goal: @Perp Tn C D A D *)
  apply perp_comm, (sac__perp1214 _ _ B), sac_perm; trivial.
Qed.

Lemma cop_sac2__sac : forall A B C D E F,
  Saccheri A B C D -> Saccheri A B E F -> D<>F -> Coplanar A B D F -> Saccheri D C E F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Saccheri Tn A B E F) (_ : not (@eq (@Tpoint Tn) D F)) (_ : @Coplanar Tn A B D F), @Saccheri Tn D C E F *)
  intros A B C D E F HSac HSac2 HDF HCop.
(* Goal: @Saccheri Tn D C E F *)
  assert(HPerp := sac__perp1214 _ _ _ _ HSac); assert(HPerp2 := sac__perp1214 _ _ _ _ HSac2).
(* Goal: @Saccheri Tn D C E F *)
  assert(HPerp3 := sac__perp3414 _ _ _ _ HSac); assert(HPerp4 := sac__perp3414 _ _ _ _ HSac2).
(* Goal: @Saccheri Tn D C E F *)
  assert(Col A D F).
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
    apply cop_perp2__col with A B; Perp.
(* Goal: @Saccheri Tn D C E F *)
  assert(Hdiff := sac_distincts _ _ _ _ HSac).
(* Goal: @Saccheri Tn D C E F *)
  assert(Hdiff2 := sac_distincts _ _ _ _ HSac2).
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  unfold Saccheri in *; spliter; repeat split.
  - apply perp_per_1; auto.
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
    apply perp_col0 with D A; Col; Perp.
  - apply perp_per_1; auto.
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
    apply perp_sym, perp_col0 with F A; Col; Perp.
  - apply cong_transitivity with A B; Cong.
  - apply one_side_transitivity with B.
(* Goal: @OS Tn D F C B *)
(* Goal: @OS Tn D F B E *)
      apply col_one_side with A; Col; Side.
(* Goal: @OS Tn D F B E *)
    apply invert_one_side, col_one_side with A; Col; Side.
Qed.

(** This comes from Martin's proof in Theorem 22.10 *)

Lemma three_hypotheses_aux : forall A B C D M N A' B' C' D' M' N',
  Saccheri A B C D -> Saccheri A' B' C' D' ->
  Midpoint M B C -> Midpoint M' B' C' -> Midpoint N A D -> Midpoint N' A' D' ->
  Le M N M' N' ->
  (Per A B C <-> Per A' B' C') /\ (Acute A B C <-> Acute A' B' C').
Proof.
(* Goal: forall (A B C D M N A' B' C' D' M' N' : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Saccheri Tn A' B' C' D') (_ : @Midpoint Tn M B C) (_ : @Midpoint Tn M' B' C') (_ : @Midpoint Tn N A D) (_ : @Midpoint Tn N' A' D') (_ : @Le Tn M N M' N'), and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  intros A B C D M N A' B' C' D' M' N' HSac HSac' HM HM' HN HN' Hle.
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(HLam1 := mid2_sac__lam6534 A B C D M N HSac HM HN).
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(HLam1' := mid2_sac__lam6534 A' B' C' D' M' N' HSac' HM' HN').
(* Goal: @LtA Tn B D C A B D *)
  assert(Hdiff := sac_distincts A B C D HSac).
(* Goal: @Obtuse Tn A' B' C' *)
  assert(Hdiff' := sac_distincts A' B' C' D' HSac').
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(HNCol1 : ~ Col A C D) by (apply (sac__ncol134 _ B); auto).
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  rename H into HA'B'.
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(HH := segment_construction_3 N D N' D').
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  destruct HH as [H []]; auto.
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(Col A D H) by ColR.
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(G0 := l10_15 A D H C).
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  destruct G0 as [G0 []]; Col.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(HG := segment_construction_3 H G0 C' D').
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  destruct HG as [G []]; auto.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(OS N D C G).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { apply invert_one_side.
(* Goal: @OS Tn D N C G *)
    apply (col_one_side _ A); Col.
(* Goal: @OS Tn B C A D *)
    apply invert_one_side.
(* Goal: @OS Tn A D C G *)
    apply (one_side_transitivity _ _ _ G0); auto.
(* Goal: False *)
(* Goal: False *)
    apply(l9_19 _ _ _ _ H); assert_cols; Col.
(* Goal: and (@SumA Tn C A B A B C D E F) (@SumA Tn D E F B C A D E D') *)
    split; auto.
(* Goal: not (@Col Tn A D G0) *)
    apply (one_side_not_col123 _ _ _ C); Side.
  }
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(Perp A D H G) by (assert_cols; apply (perp_col1 _ _ _ G0); Perp; Col).
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  clear dependent G0.
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(HNCol2 : ~ Col M N H).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { unfold Lambert in HLam1.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: not (@Col Tn M N H) *)
    apply per_not_col; auto.
(* Goal: @Per Tn M N H *)
    apply (per_col _ _ D); auto; ColR.
  }
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert (HCop : Coplanar A D M G).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { apply coplanar_trans_1 with C; Col.
(* Goal: @Coplanar Tn C A D M *)
(* Goal: @Coplanar Tn C A D G *)
      assert (~ Col B C D) by (apply (sac__ncol234 A), HSac).
(* Goal: @Coplanar Tn C A D M *)
(* Goal: @Coplanar Tn C A D G *)
      apply sac__coplanar in HSac.
(* Goal: @Coplanar Tn C A D M *)
(* Goal: @Coplanar Tn C A D G *)
      apply coplanar_perm_12, col_cop__cop with B; Col; Cop.
(* Goal: @Coplanar Tn C A D G *)
    apply coplanar_perm_5, col_cop__cop with N; Col; Cop.
  }
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert (HNCol3 : ~ Col M N G).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { unfold Lambert in HLam1.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: not (@Col Tn M N G) *)
    apply (one_side_not_col123 _ _ _ H).
(* Goal: @OS Tn K H C D *)
    apply l12_6.
(* Goal: @Par_strict Tn M N G H *)
    apply (par_not_col_strict _ _ _ _ H); Col.
(* Goal: @Par Tn M N G H *)
    apply (l12_9 _ _ _ _ A D); Cop; [|Perp].
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
    apply perp_right_comm; apply (perp_col1 _ _ _ N); Col; Perp.
  }
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(A <> H) by (intro; subst H; assert(Habs := l6_4_1 D A N); destruct Habs; Between).
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(Col H A N) by ColR.
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(HL := l8_18_existence M N G).
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  destruct HL as [L []]; auto.
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(HNCol4 : ~ Col M A D).
(* Goal: not (@Col Tn M A D) *)
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
    apply sac__par_strict1423 in HSac; apply (par_not_col B C); Par; Col.
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(HLam2 : Lambert N L G H).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { assert(Per N H G).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { apply (l8_3 A); Col.
(* Goal: @Per Tn A N M *)
      apply (perp_per_1); auto.
(* Goal: @Perp Tn H A G H *)
      apply perp_comm.
(* Goal: @Perp Tn A N M N *)
      apply (perp_col _ D); Col.
    }
(* Goal: @Lambert Tn N L G H *)
    assert(~ Col N H G) by (apply per_not_col; auto).
(* Goal: @Lambert Tn N L G H *)
    assert(Per A N M).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { apply perp_per_1; auto.
(* Goal: @Perp Tn N A M N *)
      apply perp_left_comm.
(* Goal: @Perp Tn A N M N *)
      apply (perp_col _ D); Col.
(* Goal: @Perp Tn A D M N *)
      apply (mid2_sac__perp_lower _ B C); auto.
    }
(* Goal: @Lambert Tn N L G H *)
    assert(Per L N H) by (apply (l8_3 M); Col; apply (per_col _ _ A); Col; Perp).
(* Goal: @Lambert Tn N L G H *)
    assert(N <> L).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { intro.
(* Goal: @ex (@Tpoint Tn) (fun K : @Tpoint Tn => and (@Col Tn K M C) (@Bet Tn G K H)) *)
      subst L.
(* Goal: False *)
      assert(Col G H N); Col.
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
      apply cop_per2__col with M; [|Perp..|apply (l8_3 A); Col].
(* Goal: @Coplanar Tn M G H N *)
      apply coplanar_pseudo_trans with A D M; Cop; Col.
    }
(* Goal: @SAMS Tn B C A A C D *)
    repeat split; auto.
(* Goal: False *)
(* Goal: False *)
      intro; subst; assert_cols; Col.
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
      apply perp_per_1; auto; apply perp_left_comm, (perp_col _ M); Col; Perp.
(* Goal: @Coplanar Tn N L G H *)
      apply coplanar_pseudo_trans with A D M; [Col|Cop| |Cop..].
(* Goal: and (@Col Tn I A D) (@Bet Tn B I C) *)
      exists N; left; split; Col.
  }
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(Par_strict N D M C) by (apply lam__par_strict1423, HLam1).
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(Bet N M L).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { assert(HCong := cong2_lam2__cong N' M' C' D' N L G H).
(* Goal: @Bet Tn N M L *)
    apply l6_13_1; [|apply (l5_6 M N M' N'); Cong].
(* Goal: @Out Tn C K M *)
    apply (col_one_side_out _ D); Col.
(* Goal: @OS Tn N D M L *)
    apply (one_side_transitivity _ _ _ G).
(* Goal: @OS Tn N D M G *)
(* Goal: @OS Tn N D G L *)
      apply (one_side_transitivity _ _ _ C); auto; apply l12_6; auto.
(* Goal: @OS Tn N D G L *)
    apply (col_one_side _ H); auto; try ColR.
(* Goal: @OS Tn N H G L *)
    apply one_side_symmetry, l12_6, lam__par_strict1423, HLam2.
  }
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(HNCol5 : ~ Col N M C) by (unfold Lambert in HLam1; spliter; apply per_not_col; auto).
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(HNCol6 : ~ Col N D M) by (apply (par_strict_not_col_1 _ _ _ C); auto).
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert (Coplanar M C D A).
(* Goal: @Coplanar Tn M C D A *)
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
    apply pars__coplanar, par_strict_col_par_strict with N; Col; Par.
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(HK : exists K, Col K M C /\ Bet G K H).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { elim(eq_dec_points L M).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { intro.
(* Goal: @ex (@Tpoint Tn) (fun K : @Tpoint Tn => and (@Col Tn K M C) (@Bet Tn G K H)) *)
      subst L.
(* Goal: @ex (@Tpoint Tn) (fun K : @Tpoint Tn => and (@Col Tn K M C) (@Bet Tn G K H)) *)
      exists G.
(* Goal: and (@Col Tn G M C) (@Bet Tn G G H) *)
      split; Between.
(* Goal: @Col Tn G M C *)
      apply col_permutation_5.
(* Goal: False *)
      unfold Lambert in *.
(* Goal: @LtA Tn A C D B A C *)
      spliter.
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
      apply cop_per2__col with N; Perp.
(* Goal: @Coplanar Tn M N C G *)
      apply coplanar_pseudo_trans with A D M; Col; Cop.
    }
(* Goal: forall _ : @Obtuse Tn A C B, hypothesis_of_obtuse_saccheri_quadrilaterals *)
    intro.
(* Goal: @ex (@Tpoint Tn) (fun K : @Tpoint Tn => and (@Col Tn K M C) (@Bet Tn G K H)) *)
    assert(HNCol7 : ~ Col L M C) by (intro; apply HNCol5; ColR).
(* Goal: @ex (@Tpoint Tn) (fun K : @Tpoint Tn => and (@Col Tn K M C) (@Bet Tn G K H)) *)
    assert(Hts : TS M C G H); [|unfold TS in Hts; spliter; auto].
(* Goal: @TS Tn M C G H *)
    apply (l9_8_2 _ _ L).
    - apply l9_2.
(* Goal: @TS Tn M C H L *)
      apply (l9_8_2 _ _ N).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Midpoint Tn X B C) (@Col Tn M N X)) *)
(* Goal: or (@Perp Tn M N B C) (@eq (@Tpoint Tn) B C) *)
        repeat split; Col; exists M; Col.
(* Goal: @OS Tn M C N H *)
      apply l12_6, (par_strict_col_par_strict _ _ _ D); Par; ColR.
    - apply l12_6, (par_not_col_strict _ _ _ _ L); Col.
(* Goal: False *)
      unfold Lambert in *.
(* Goal: @LtA Tn A C D B A C *)
      spliter.
(* Goal: @Par Tn M C L G *)
      apply (l12_9 _ _ _ _ M N); Perp; [Cop..|].
(* Goal: @Coplanar Tn M N C G *)
      apply coplanar_pseudo_trans with A D M; Col; Cop.
  }
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  destruct HK as [K []].
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(HNCol7 : ~ Col H M C) by (apply (par_not_col N D); Col).
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(K <> H) by (intro; subst K; auto).
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(Par_strict N M C D) by (apply lam__par_strict1234, HLam1).
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(HNCol8 : ~ Col N C D) by (apply (par_strict_not_col_2 M); Par).
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(Par_strict M N H K).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { apply par_strict_col_par_strict with G; Col.
(* Goal: @Par_strict Tn M N H G *)
    apply par_strict_comm, par_strict_symmetry, par_strict_col_par_strict with L; Col.
(* Goal: @Par_strict Tn G H N L *)
    apply par_strict_symmetry, lam__par_strict1234, HLam2.
  }
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(HNCol9 : ~ Col N H K) by (apply (par_strict_not_col_2 M); auto).
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(HMout : Out M C K).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { apply (col_one_side_out _ N); Col.
(* Goal: @OS Tn M N C K *)
    apply (one_side_transitivity _ _ _ D).
(* Goal: @OS Tn M N C D *)
(* Goal: @OS Tn M N D K *)
      apply l12_6; Par.
(* Goal: @OS Tn M N D K *)
    apply (one_side_transitivity _ _ _ H).
(* Goal: @OS Tn B J R C *)
      apply invert_one_side; apply out_one_side; Col.
(* Goal: @OS Tn M N H K *)
    apply l12_6; auto.
  }
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(HLam3 : Lambert N M K H).
(* Goal: False *)
  { unfold Lambert in *.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: @SAMS Tn B C A A C D *)
    repeat split; auto.
(* Goal: @Per Tn M N H *)
(* Goal: @Per Tn N H K *)
(* Goal: @Per Tn N M K *)
(* Goal: @Coplanar Tn N M K H *)
      apply (l8_3 L); Col.
(* Goal: @Per Tn N H K *)
(* Goal: @Per Tn N M K *)
(* Goal: @Coplanar Tn N M K H *)
      apply (per_col _ _ G); Col.
(* Goal: @Per Tn N M K *)
(* Goal: @Coplanar Tn N M K H *)
      apply (per_col _ _ C); Col.
(* Goal: @Coplanar Tn N M K H *)
      apply coplanar_perm_7, pars__coplanar; assumption.
  }
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(HConga := sac__conga A B C D HSac).
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(CongA A' B' C' H G L).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { apply (conga_trans _ _ _ M' C' D').
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { apply (out_conga A' B' C' B' C' D'); try (apply out_trivial); try (apply sac__conga); auto.
(* Goal: @Out Tn C B C' *)
      apply l6_6; apply bet_out; Between.
    }
(* Goal: @CongA Tn M' C' D' H G L *)
    apply conga_right_comm.
(* Goal: @CongA Tn M' C' D' L G H *)
    apply (cong2_lam2__conga N' _ _ _ N); Cong.
  }
(* Goal: and (iff (@Per Tn A B C) (@Per Tn A' B' C')) (iff (@Acute Tn A B C) (@Acute Tn A' B' C')) *)
  assert(HPar : Par C D K H).
(* Goal: False *)
  { unfold Lambert in *.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: @Par Tn C D K H *)
    apply (l12_9 _ _ _ _ N D); [|Cop..].
(* Goal: @Coplanar Tn N D C K *)
(* Goal: @Perp Tn C D N D *)
(* Goal: @Perp Tn K H N D *)
      destruct (eq_dec_points C K).
(* Goal: @Coplanar Tn N D C K *)
(* Goal: @Coplanar Tn N D C K *)
(* Goal: @Perp Tn C D N D *)
(* Goal: @Perp Tn K H N D *)
        subst; Cop.
(* Goal: @Coplanar Tn N D C K *)
(* Goal: @Perp Tn C D N D *)
(* Goal: @Perp Tn K H N D *)
      apply pars__coplanar, par_strict_col_par_strict with M; Col; Par.
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
      Perp.
(* Goal: @Perp Tn K H N D *)
    apply perp_comm, (perp_col _ G); Col; apply (perp_col1 _ _ _ A); Perp; Col.
  }
  assert(Bet M C K -> Bet N D H).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { intro.
(* Goal: @Bet Tn N D H *)
    destruct(eq_dec_points D H) as [|HDH].
(* Goal: @Bet Tn N D H *)
(* Goal: @Bet Tn N D H *)
      subst; Between.
(* Goal: @Bet Tn N H D *)
    apply between_symmetry.
(* Goal: @Bet Tn D H N *)
    apply not_out_bet; Col.
(* Goal: forall _ : @Obtuse Tn A C B, hypothesis_of_obtuse_saccheri_quadrilaterals *)
    intro.
    assert(Out C K M);
    [|assert(Habs := l6_4_1 K M C); destruct Habs; Between].
(* Goal: @Out Tn C K M *)
    apply (col_one_side_out _ D); Col.
(* Goal: @OS Tn K H C M *)
    apply (one_side_transitivity _ _ _ N); [|apply l12_6; Par].
(* Goal: @OS Tn C D K N *)
    apply (one_side_transitivity _ _ _ H); [|apply invert_one_side; apply out_one_side; Col].
(* Goal: @OS Tn K H C D *)
    apply l12_6.
(* Goal: @Par_strict Tn C D K H *)
    destruct HPar; auto.
(* Goal: hypothesis_of_obtuse_saccheri_quadrilaterals *)
    exfalso.
(* Goal: False *)
    unfold Lambert in *.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: False *)
    apply HDH.
(* Goal: @eq (@Tpoint Tn) D H *)
    apply (l8_18_uniqueness C D N); Col.
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
      Perp.
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
      ColR.
(* Goal: @Perp Tn C D N H *)
    apply (perp_col _ H); auto; [|ColR].
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
    apply perp_left_comm, (perp_col _ G); Perp; ColR.
  }
  assert(Bet M K C -> Bet N H D).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { intro.
(* Goal: @Bet Tn N H D *)
    elim(eq_dec_points D H).
(* Goal: @Bet Tn N D H *)
(* Goal: @Bet Tn N D H *)
      intro; subst; Between.
(* Goal: forall _ : not (@eq (@Tpoint Tn) D H), @Bet Tn N H D *)
    intro HDH.
(* Goal: @Bet Tn N H D *)
    apply between_symmetry.
(* Goal: @Bet Tn D H N *)
    apply not_out_bet; Col.
(* Goal: forall _ : @Obtuse Tn A C B, hypothesis_of_obtuse_saccheri_quadrilaterals *)
    intro.
(* Goal: False *)
    assert(Out K C M); [|assert(Habs := l6_4_1 C M K); destruct Habs; Between].
(* Goal: @Out Tn K C M *)
    apply (col_one_side_out _ H); Col.
(* Goal: @OS Tn K H C M *)
    apply (one_side_transitivity _ _ _ N); [|apply l12_6; Par].
(* Goal: @OS Tn K H C N *)
    apply (one_side_transitivity _ _ _ D); [|apply invert_one_side; apply out_one_side; Col].
(* Goal: @OS Tn K H C D *)
    apply l12_6.
(* Goal: @Par_strict Tn K H C D *)
    destruct HPar; Par.
(* Goal: hypothesis_of_obtuse_saccheri_quadrilaterals *)
    exfalso.
(* Goal: False *)
    unfold Lambert in *.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: False *)
    apply HDH.
(* Goal: @eq (@Tpoint Tn) D H *)
    apply (l8_18_uniqueness C D N); Col.
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
      Perp.
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
      ColR.
(* Goal: @Perp Tn C D N H *)
    apply (perp_col _ H); auto; [|ColR].
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
    apply perp_left_comm, (perp_col _ G); Perp; ColR.
  }
(* Goal: forall _ : @Obtuse Tn A C B, hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split; split; intro.

  - apply (l11_17 L G H); CongA.
(* Goal: @Per Tn L G H *)
    apply (t22_9__per N _ K M); try (apply lam_perm); Between.
(* Goal: @Per Tn C' C D *)
    apply l8_2.
(* Goal: @Per Tn H K M *)
    assert(Per D C M).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { apply (l11_17 A B C); auto.
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
      apply (out_conga A B C D C B); try (apply out_trivial); CongA.
(* Goal: @Out Tn C B M *)
      apply l6_6.
(* Goal: @Out Tn C B C' *)
      apply bet_out; Between.
    }
(* Goal: @Acute Tn D C M *)
    destruct HMout as [_ [_ [HMCK|HMKC]]].
(* Goal: @Per Tn H K M *)
(* Goal: @Per Tn H K M *)
      apply (t22_9__per N _ C D); auto.
(* Goal: @Per Tn H K M *)
      apply (t22_9__per N _ _ _ C D); auto.

  - apply (l11_17 D C M).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { assert(Per H K M).
(* Goal: @Per Tn H K M *)
(* Goal: @Per Tn D C M *)
        apply l8_2, (t22_9__per N _ _ _ G L); try (apply lam_perm); Between.
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
        apply (l11_17 A' B' C'); CongA.
(* Goal: @Acute Tn D C M *)
      destruct HMout as [_ [_ [HMCK|HMKC]]].
(* Goal: @Per Tn D C M *)
(* Goal: @Per Tn D C M *)
        apply (t22_9__per N _ _ _ K H); auto.
(* Goal: @Per Tn D C M *)
        apply (t22_9__per N _ K H); auto.
    }
(* Goal: @CongA Tn D C M A B C *)
    apply (out_conga D C B A B C); try (apply out_trivial); CongA.
(* Goal: @Out Tn C B M *)
    apply l6_6, bet_out; Between.

  - apply (acute_conga__acute L G H); CongA.
(* Goal: @Acute Tn L G H *)
    apply (t22_9__acute N _ K M); try (apply lam_perm); Between.
(* Goal: @Acute Tn H K M *)
(* Goal: @Acute Tn D C M *)
    apply acute_sym.
(* Goal: @Acute Tn H K M *)
    assert(Acute D C M).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { apply (acute_conga__acute A B C); auto.
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
      apply (out_conga A B C D C B); try (apply out_trivial); CongA.
(* Goal: @Out Tn C B M *)
      apply l6_6.
(* Goal: @Out Tn C B C' *)
      apply bet_out; Between.
    }
(* Goal: @Acute Tn D C M *)
    destruct HMout as [_ [_ [HMCK|HMKC]]].
(* Goal: @Acute Tn H K M *)
(* Goal: @Acute Tn H K M *)
      apply (t22_9__acute N _ C D); auto.
(* Goal: @Acute Tn H K M *)
      apply (t22_9__acute N _ _ _ C D); auto.

  - apply (acute_conga__acute D C M).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { assert(Acute H K M).
(* Goal: @Acute Tn H K M *)
(* Goal: @Acute Tn D C M *)
        apply acute_sym.
(* Goal: @Acute Tn M K H *)
(* Goal: @Acute Tn D C M *)
          apply (t22_9__acute N _ _ _ G L); try (apply lam_perm); Between.
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
          apply (acute_conga__acute A' B' C'); CongA.
(* Goal: @Acute Tn D C M *)
      destruct HMout as [_ [_ [HMCK|HMKC]]].
(* Goal: @Acute Tn D C M *)
(* Goal: @Acute Tn D C M *)
        apply (t22_9__acute N _ _ _ K H); auto.
(* Goal: @Acute Tn D C M *)
        apply (t22_9__acute N _ K H); auto.
    }
(* Goal: @CongA Tn D C M A B C *)
    apply (out_conga D C B A B C); try (apply out_trivial); CongA.
(* Goal: @Out Tn C B M *)
    apply l6_6, bet_out; Between.
Qed.


(** Saccheri's three hypotheses *)

Definition hypothesis_of_right_saccheri_quadrilaterals := forall A B C D, Saccheri A B C D -> Per A B C.

Definition hypothesis_of_acute_saccheri_quadrilaterals := forall A B C D, Saccheri A B C D -> Acute A B C.

Definition hypothesis_of_obtuse_saccheri_quadrilaterals := forall A B C D, Saccheri A B C D -> Obtuse A B C.

Lemma per_sac__rah : forall A B C D,
  Saccheri A B C D -> Per A B C -> hypothesis_of_right_saccheri_quadrilaterals.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Obtuse Tn A B C), hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intros A B C D HSac HPer A' B' C' D' HSac'.
(* Goal: @Acute Tn A' B' C' *)
  assert(HM := midpoint_existence B C).
(* Goal: @Acute Tn A' B' C' *)
  assert(HM' := midpoint_existence B' C').
(* Goal: @Acute Tn A' B' C' *)
  assert(HN := midpoint_existence A D).
(* Goal: @Acute Tn A' B' C' *)
  assert(HN' := midpoint_existence A' D').
(* Goal: @Acute Tn A' B' C' *)
  destruct HM as [M].
(* Goal: @Acute Tn A' B' C' *)
  destruct HM' as [M'].
(* Goal: @Acute Tn A' B' C' *)
  destruct HN as [N].
(* Goal: @Acute Tn A' B' C' *)
  destruct HN' as [N'].
  elim(le_cases M N M' N');
  intro Hle;
  [assert(Haux := three_hypotheses_aux A B C D M N A' B' C' D' M' N')
  |assert(Haux := three_hypotheses_aux A' B' C' D' M' N' A B C D M N)];
  destruct Haux as [[] _]; auto.
Qed.

Lemma acute_sac__aah : forall A B C D,
  Saccheri A B C D -> Acute A B C -> hypothesis_of_acute_saccheri_quadrilaterals.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Obtuse Tn A B C), hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intros A B C D HSac HPer A' B' C' D' HSac'.
(* Goal: @Acute Tn A' B' C' *)
  assert(HM := midpoint_existence B C).
(* Goal: @Acute Tn A' B' C' *)
  assert(HM' := midpoint_existence B' C').
(* Goal: @Acute Tn A' B' C' *)
  assert(HN := midpoint_existence A D).
(* Goal: @Acute Tn A' B' C' *)
  assert(HN' := midpoint_existence A' D').
(* Goal: @Acute Tn A' B' C' *)
  destruct HM as [M].
(* Goal: @Acute Tn A' B' C' *)
  destruct HM' as [M'].
(* Goal: @Acute Tn A' B' C' *)
  destruct HN as [N].
(* Goal: @Acute Tn A' B' C' *)
  destruct HN' as [N'].
  elim(le_cases M N M' N');
  intro Hle;
  [assert(Haux := three_hypotheses_aux A B C D M N A' B' C' D' M' N')
  |assert(Haux := three_hypotheses_aux A' B' C' D' M' N' A B C D M N)];
  destruct Haux as [_ []]; auto.
Qed.

Lemma obtuse_sac__oah : forall A B C D,
  Saccheri A B C D -> Obtuse A B C -> hypothesis_of_obtuse_saccheri_quadrilaterals.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Obtuse Tn A B C), hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intros A B C D HSac HPer A' B' C' D' HSac'.
(* Goal: @LtA Tn B D C A B D *)
  assert(Hdiff := sac_distincts A B C D HSac).
(* Goal: @Obtuse Tn A' B' C' *)
  assert(Hdiff' := sac_distincts A' B' C' D' HSac').
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: @Obtuse Tn A' B' C' *)
  elim(angle_partition A' B' C'); auto.
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { intro Hacute'.
(* Goal: hypothesis_of_obtuse_saccheri_quadrilaterals *)
    exfalso.
(* Goal: False *)
    apply (nlta A B C).
(* Goal: @LtA Tn A B C A B C *)
    apply (acute_obtuse__lta); auto.
(* Goal: @Acute Tn A B C *)
    assert(aah := acute_sac__aah A' B' C' D' HSac' Hacute').
(* Goal: @Acute Tn A B C *)
    apply (aah _ _ _ D); auto.
  }
(* Goal: forall _ : or (@Per Tn A' B' C') (@Obtuse Tn A' B' C'), @Obtuse Tn A' B' C' *)
  intro HUn.
(* Goal: @Obtuse Tn A' B' C' *)
  destruct HUn as [HPer'|]; auto.
(* Goal: hypothesis_of_obtuse_saccheri_quadrilaterals *)
  exfalso.
(* Goal: False *)
  apply (nlta A B C).
(* Goal: @LtA Tn B C D P Q R *)
(* Goal: @SAMS Tn B C A A C D *)
(* Goal: @SumA Tn B C A A C D B C D *)
  apply (obtuse_per__lta); auto.
(* Goal: @Per Tn A B C *)
  assert(rah := per_sac__rah A' B' C' D' HSac' HPer').
(* Goal: @Per Tn A B C *)
  apply (rah _ _ _ D); auto.
Qed.

Lemma per__ex_saccheri : forall A B D, Per B A D -> A <> B -> A <> D ->
  exists C, Saccheri A B C D.
Proof.
(* Goal: forall (A B D : @Tpoint Tn) (_ : @Per Tn B A D) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) A D)), @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @Saccheri Tn A B C D) *)
  intros A B D HPer HAB HBD.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @Saccheri Tn A B C D) *)
  assert (HNCol : ~ Col B A D) by (apply per_not_col; auto).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @Saccheri Tn A B C D) *)
  destruct (l10_15 A D D B) as [C0 []]; Col.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @Saccheri Tn A B C D) *)
  assert(~ Col A D C0) by (apply (one_side_not_col123 _ _ _ B); Side).
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @Saccheri Tn A B C D) *)
  destruct (segment_construction_3 D C0 A B) as [C []]; auto.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Per Tn B B' C') (@GtA Tn P Q R B B' C'))) *)
  exists C.
(* Goal: @Saccheri Tn B A D C *)
  repeat split; Cong.
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
    apply (per_col _ _ C0); Col; Perp.
(* Goal: @OS Tn A D B C *)
    apply invert_one_side; apply (out_out_one_side _ _ _ C0); Side.
Qed.

Lemma ex_saccheri : exists A B C D, Saccheri A B C D.
Proof.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Saccheri Tn A B C D)))) *)
  destruct lower_dim_ex as [A [D [E]]].
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Saccheri Tn A B C D)))) *)
  assert(HNCol : ~ Col A D E) by (unfold Col; assumption).
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Saccheri Tn A B C D)))) *)
  destruct (l10_15 A D A E) as [B []]; Col.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Saccheri Tn A B C D)))) *)
  assert(~ Col A D B) by (apply (one_side_not_col123 _ _ _ E); Side).
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
  destruct (per__ex_saccheri A B D) as [C HSac]; Perp.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Saccheri Tn A B C D)))) *)
  exists A; exists B; exists C; exists D; trivial.
Qed.

Lemma ex_lambert : exists A B C D, Lambert A B C D.
Proof.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Lambert Tn A B C D)))) *)
  destruct ex_saccheri as [D [C [C' [D' HSac]]]].
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Lambert Tn A B C D)))) *)
  destruct (midpoint_existence D D') as [A HA].
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Lambert Tn A B C D)))) *)
  destruct (midpoint_existence C C') as [B HB].
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Lambert Tn A B C D)))) *)
  exists A, B, C, D.
(* Goal: @Lambert Tn A B C D *)
  apply mid2_sac__lam6521 with C' D'; trivial.
Qed.

Lemma saccheri_s_three_hypotheses :
  hypothesis_of_acute_saccheri_quadrilaterals \/ hypothesis_of_right_saccheri_quadrilaterals \/ hypothesis_of_obtuse_saccheri_quadrilaterals.
Proof.
(* Goal: False *)
  destruct ex_saccheri as [A [B [C [D HSac]]]].
(* Goal: @LtA Tn B D C A B D *)
  assert(Hdiff := sac_distincts A B C D HSac).
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: or hypothesis_of_acute_saccheri_quadrilaterals (or hypothesis_of_right_saccheri_quadrilaterals hypothesis_of_obtuse_saccheri_quadrilaterals) *)
  elim(angle_partition A B C); auto; [|intro HUn; destruct HUn].
(* Goal: forall _ : @Acute Tn A B C, or hypothesis_of_acute_saccheri_quadrilaterals (or hypothesis_of_right_saccheri_quadrilaterals hypothesis_of_obtuse_saccheri_quadrilaterals) *)
(* Goal: or hypothesis_of_acute_saccheri_quadrilaterals (or hypothesis_of_right_saccheri_quadrilaterals hypothesis_of_obtuse_saccheri_quadrilaterals) *)
(* Goal: or hypothesis_of_acute_saccheri_quadrilaterals (or hypothesis_of_right_saccheri_quadrilaterals hypothesis_of_obtuse_saccheri_quadrilaterals) *)
    intro; left; apply (acute_sac__aah A B C D); trivial.
(* Goal: or hypothesis_of_acute_saccheri_quadrilaterals (or hypothesis_of_right_saccheri_quadrilaterals hypothesis_of_obtuse_saccheri_quadrilaterals) *)
(* Goal: or hypothesis_of_acute_saccheri_quadrilaterals (or hypothesis_of_right_saccheri_quadrilaterals hypothesis_of_obtuse_saccheri_quadrilaterals) *)
    right; left; apply (per_sac__rah A B C D); trivial.
(* Goal: or hypothesis_of_acute_saccheri_quadrilaterals (or hypothesis_of_right_saccheri_quadrilaterals hypothesis_of_obtuse_saccheri_quadrilaterals) *)
  right; right; apply (obtuse_sac__oah A B C D); trivial.
Qed.

Lemma not_aah :
  hypothesis_of_right_saccheri_quadrilaterals \/ hypothesis_of_obtuse_saccheri_quadrilaterals -> ~ hypothesis_of_acute_saccheri_quadrilaterals.
Proof.
(* Goal: forall _ : or hypothesis_of_right_saccheri_quadrilaterals hypothesis_of_obtuse_saccheri_quadrilaterals, not hypothesis_of_acute_saccheri_quadrilaterals *)
  intros HUn aah.
(* Goal: False *)
  destruct ex_saccheri as [A [B [C [D HSac]]]].
(* Goal: @LtA Tn B D C A B D *)
  assert(Hdiff := sac_distincts A B C D HSac).
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: False *)
  apply (nlta A B C).
(* Goal: @LtA Tn A B C A B C *)
  assert(Acute A B C) by (apply (aah _ _ _ D); auto).
(* Goal: @LtA Tn A B C A B C *)
  destruct HUn as [rah|oah].
  - apply (acute_per__lta); auto.
(* Goal: @Per Tn A B C *)
    apply (rah _ _ _ D); auto.

  - apply (acute_obtuse__lta); auto.
(* Goal: @Obtuse Tn A B C *)
    apply (oah _ _ _ D); auto.
Qed.

Lemma not_rah :
  hypothesis_of_acute_saccheri_quadrilaterals \/ hypothesis_of_obtuse_saccheri_quadrilaterals -> ~ hypothesis_of_right_saccheri_quadrilaterals.
Proof.
(* Goal: forall _ : or hypothesis_of_acute_saccheri_quadrilaterals hypothesis_of_obtuse_saccheri_quadrilaterals, not hypothesis_of_right_saccheri_quadrilaterals *)
  intros HUn rah.
(* Goal: False *)
  destruct ex_saccheri as [A [B [C [D HSac]]]].
(* Goal: @LtA Tn B D C A B D *)
  assert(Hdiff := sac_distincts A B C D HSac).
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: False *)
  apply (nlta A B C).
(* Goal: @LtA Tn A B C A B C *)
  assert(Per A B C) by (apply (rah _ _ _ D); auto).
(* Goal: @LtA Tn A B C A B C *)
  destruct HUn as [aah|oah].
  - apply (acute_per__lta); auto.
(* Goal: @Acute Tn A B C *)
    apply (aah _ _ _ D); auto.

  - apply (obtuse_per__lta); auto.
(* Goal: @Obtuse Tn A B C *)
    apply (oah _ _ _ D); auto.
Qed.

Lemma not_oah :
  hypothesis_of_acute_saccheri_quadrilaterals \/ hypothesis_of_right_saccheri_quadrilaterals -> ~ hypothesis_of_obtuse_saccheri_quadrilaterals.
Proof.
(* Goal: forall _ : or hypothesis_of_acute_saccheri_quadrilaterals hypothesis_of_right_saccheri_quadrilaterals, not hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intros HUn oah.
(* Goal: False *)
  destruct ex_saccheri as [A [B [C [D HSac]]]].
(* Goal: @LtA Tn B D C A B D *)
  assert(Hdiff := sac_distincts A B C D HSac).
(* Goal: @LtA Tn A C D B A C *)
  spliter.
(* Goal: False *)
  apply (nlta A B C).
(* Goal: @LtA Tn A B C A B C *)
  assert(Obtuse A B C) by (apply (oah _ _ _ D); auto).
(* Goal: @LtA Tn A B C A B C *)
  destruct HUn as [aah|rah].
  - apply (acute_obtuse__lta); auto.
(* Goal: @Acute Tn A B C *)
    apply (aah _ _ _ D); auto.

  - apply (obtuse_per__lta); auto.
(* Goal: @Per Tn A B C *)
    apply (rah _ _ _ D); auto.
Qed.


Lemma lam_per__rah : forall A B C D,
  Lambert A B C D -> (Per B C D <-> hypothesis_of_right_saccheri_quadrilaterals).
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Lambert Tn A B C D), iff (@Obtuse Tn B C D) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intros A B C D HLam.
(* Goal: iff (@Obtuse Tn B C D) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HC' := symmetric_point_construction C B).
(* Goal: iff (@Obtuse Tn B C D) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  destruct HC' as [C'].
(* Goal: iff (@Obtuse Tn B C D) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HD' := symmetric_point_construction D A).
(* Goal: iff (@Obtuse Tn B C D) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  destruct HD' as [D'].
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split.
  - intro.
(* Goal: hypothesis_of_right_saccheri_quadrilaterals *)
    apply (per_sac__rah D C C' D').
(* Goal: @Saccheri Tn D C C' D' *)
(* Goal: @Obtuse Tn D C C' *)
      apply (lam6521_mid2__sac _ _ _ _ B A); auto.
(* Goal: @CongA Tn D C C' B C D *)
    unfold Lambert in HLam.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: @Per Tn C' C D *)
    apply l8_2.
(* Goal: @Per Tn C' C D *)
    apply (l8_3 B); Col.

  - intro rah.
(* Goal: @Per Tn B C D *)
    apply (l8_3 C'); Col ;[|unfold Lambert in HLam; spliter; assert_diffs; auto].
(* Goal: @Per Tn C' C D *)
    apply l8_2.
(* Goal: @Per Tn D C C' *)
    apply (rah _ _ _ D').
(* Goal: @Saccheri Tn D C C' D' *)
(* Goal: @Obtuse Tn D C C' *)
    apply (lam6521_mid2__sac _ _ _ _ B A); auto.
Qed.

Lemma lam_acute__aah : forall A B C D,
  Lambert A B C D -> (Acute B C D <-> hypothesis_of_acute_saccheri_quadrilaterals).
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Lambert Tn A B C D), iff (@Obtuse Tn B C D) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intros A B C D HLam.
(* Goal: iff (@Obtuse Tn B C D) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HC' := symmetric_point_construction C B).
(* Goal: iff (@Obtuse Tn B C D) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  destruct HC' as [C'].
(* Goal: iff (@Obtuse Tn B C D) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HD' := symmetric_point_construction D A).
(* Goal: iff (@Obtuse Tn B C D) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  destruct HD' as [D'].
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split.
  - intro.
(* Goal: hypothesis_of_acute_saccheri_quadrilaterals *)
    apply (acute_sac__aah D C C' D').
(* Goal: @Saccheri Tn D C C' D' *)
(* Goal: @Obtuse Tn D C C' *)
      apply (lam6521_mid2__sac _ _ _ _ B A); auto.
(* Goal: @CongA Tn D C C' B C D *)
    unfold Lambert in HLam.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: @LeA Tn D E F C A B' *)
    assert_diffs.
(* Goal: @Acute Tn D C C' *)
    apply (acute_conga__acute B C D); auto.
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
    apply (out_conga B C D D C B); try (apply out_trivial); CongA.
(* Goal: @Out Tn C B C' *)
    apply bet_out; Between.

  - intro aah.
(* Goal: @Acute Tn B C D *)
    apply (acute_conga__acute D C C'); auto.
(* Goal: @Saccheri Tn D C C' D' *)
(* Goal: @Obtuse Tn D C C' *)
      apply (aah _ _ _ D'); apply (lam6521_mid2__sac _ _ _ _ B A); auto.
(* Goal: @CongA Tn D C C' B C D *)
    unfold Lambert in HLam.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: @LeA Tn D E F C A B' *)
    assert_diffs.
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
    apply (out_conga D C B B C D); try (apply out_trivial); CongA.
(* Goal: @Out Tn C B C' *)
    apply bet_out; Between.
Qed.

Lemma lam_obtuse__oah : forall A B C D,
  Lambert A B C D -> (Obtuse B C D <-> hypothesis_of_obtuse_saccheri_quadrilaterals).
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Lambert Tn A B C D), iff (@Obtuse Tn B C D) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intros A B C D HLam.
(* Goal: iff (@Obtuse Tn B C D) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HC' := symmetric_point_construction C B).
(* Goal: iff (@Obtuse Tn B C D) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  destruct HC' as [C'].
(* Goal: iff (@Obtuse Tn B C D) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HD' := symmetric_point_construction D A).
(* Goal: iff (@Obtuse Tn B C D) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  destruct HD' as [D'].
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split.
  - intro.
(* Goal: hypothesis_of_obtuse_saccheri_quadrilaterals *)
    apply (obtuse_sac__oah D C C' D').
(* Goal: @Saccheri Tn D C C' D' *)
(* Goal: @Obtuse Tn D C C' *)
      apply (lam6521_mid2__sac _ _ _ _ B A); auto.
(* Goal: @CongA Tn D C C' B C D *)
    unfold Lambert in HLam.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: @LeA Tn D E F C A B' *)
    assert_diffs.
(* Goal: @Obtuse Tn D C C' *)
    apply (conga_obtuse__obtuse B C D); auto.
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
    apply (out_conga B C D D C B); try (apply out_trivial); CongA.
(* Goal: @Out Tn C B C' *)
    apply bet_out; Between.

  - intro oah.
(* Goal: @Obtuse Tn B C D *)
    apply (conga_obtuse__obtuse D C C'); auto.
(* Goal: @Saccheri Tn D C C' D' *)
(* Goal: @Obtuse Tn D C C' *)
      apply (oah _ _ _ D'); apply (lam6521_mid2__sac _ _ _ _ B A); auto.
(* Goal: @CongA Tn D C C' B C D *)
    unfold Lambert in HLam.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: @LeA Tn D E F C A B' *)
    assert_diffs.
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
    apply (out_conga D C B B C D); try (apply out_trivial); CongA.
(* Goal: @Out Tn C B C' *)
    apply bet_out; Between.
Qed.


Lemma t22_11__per : forall A B C D,
  Saccheri A B C D -> (CongA A B D B D C <-> Per A B C).
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D), iff (@LtA Tn B D C A B D) (@Obtuse Tn A B C) *)
  intros A B C D HSac.
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split.
  - intro.
(* Goal: @Per Tn A B C *)
    apply (cong_sac__per _ _ _ D); auto.
(* Goal: @LtA Tn A C D B A C *)
    unfold Saccheri in HSac.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: @Cong Tn A D B C *)
    assert(HSAS := l11_49 A B D C D B).
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
    destruct HSAS; Cong; CongA.

  - intro HPer.
    apply <- (cong_sac__per A B C D) in HPer; trivial.
(* Goal: @LtA Tn B D C A B D *)
    assert(Hdiff := sac_distincts A B C D HSac).
(* Goal: @LtA Tn A C D B A C *)
    unfold Saccheri in HSac.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: @CongA Tn A B D B D C *)
    assert(HSSS := l11_51 A B D C D B).
(* Goal: @CongA Tn A B D B D C *)
    destruct HSSS as [_ []]; Cong; CongA.
Qed.

Lemma t22_11__acute : forall A B C D,
  Saccheri A B C D -> (LtA A B D B D C <-> Acute A B C).
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D), iff (@LtA Tn B D C A B D) (@Obtuse Tn A B C) *)
  intros A B C D HSac.
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split.
  - intro.
(* Goal: @Acute Tn A B C *)
    apply (lt_sac__acute _ _ _ D); auto.
(* Goal: @LtA Tn A C D B A C *)
    unfold Saccheri in HSac.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: @Lt Tn B C A D *)
    apply lt_right_comm.
(* Goal: @Lt Tn A D C B *)
    apply (t18_18 D _ _ B); Cong.
(* Goal: @LtA Tn C D B A B D *)
    apply lta_left_comm; auto.

  - intro Hacute.
    apply <- (lt_sac__acute A B C D) in Hacute; trivial.
(* Goal: @LtA Tn B D C A B D *)
    assert(Hdiff := sac_distincts A B C D HSac).
(* Goal: @LtA Tn A C D B A C *)
    unfold Saccheri in HSac.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: @LtA Tn B A C A C D *)
    apply lta_left_comm.
(* Goal: @LtA Tn C D B A B D *)
    apply t18_19; Cong.
(* Goal: @Lt Tn B C D A *)
    apply lt_right_comm; Cong.
Qed.

Lemma t22_11__obtuse : forall A B C D,
  Saccheri A B C D -> (LtA B D C A B D <-> Obtuse A B C).
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Saccheri Tn A B C D), iff (@LtA Tn B D C A B D) (@Obtuse Tn A B C) *)
  intros A B C D HSac.
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split.
  - intro.
(* Goal: @Obtuse Tn A B C *)
    apply (lt_sac__obtuse _ _ _ D); auto.
(* Goal: @LtA Tn A C D B A C *)
    unfold Saccheri in HSac.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: @Lt Tn B C A D *)
    apply lt_right_comm.
(* Goal: @Lt Tn B C D A *)
    apply (t18_18 B _ _ D); Cong.
(* Goal: @LtA Tn C D B A B D *)
    apply lta_left_comm; auto.

  - intro Hobtuse.
    apply <- (lt_sac__obtuse A B C D) in Hobtuse; trivial.
(* Goal: @LtA Tn B D C A B D *)
    assert(Hdiff := sac_distincts A B C D HSac).
(* Goal: @LtA Tn A C D B A C *)
    unfold Saccheri in HSac.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: @LtA Tn B A C A C D *)
    apply lta_left_comm.
(* Goal: @LtA Tn C D B A B D *)
    apply t18_19; Cong.
(* Goal: @Lt Tn B C D A *)
    apply lt_right_comm; Cong.
Qed.


Lemma t22_12__rah : forall A B C,
  A <> B -> B <> C -> Per A B C ->
  (SumA B C A C A B A B C <-> hypothesis_of_right_saccheri_quadrilaterals).
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) B C)) (_ : @Per Tn A B C), iff (@SumA Tn B C A C A B A B C) hypothesis_of_right_saccheri_quadrilaterals *)
  intros A B C HAB HBC HPer.
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(~ Col A B C) by (apply per_not_col; auto).
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HD0 := l10_15 B C C A).
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  destruct HD0 as [D0 []]; Col.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HD := segment_construction_3 C D0 A B).
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  destruct HD as [D []]; auto.
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HSac : Saccheri B A D C).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { repeat split; Cong.
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
    apply (per_col _ _ D0); Col; Perp.
(* Goal: @OS Tn B C A D *)
    apply invert_one_side.
(* Goal: @OS Tn C B A D *)
    apply (out_out_one_side _ _ _ D0); Side.
  }
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  clear dependent D0.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.

(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HPars1 := sac__par_strict1423 B A D C HSac).
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HPars2 := sac__par_strict1234 B A D C HSac).
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(TS C A B D) by (apply l9_31; apply l12_6; Par).
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(CongA B C D A B C) by (unfold Saccheri in HSac; spliter; apply l11_16; auto).
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split.
  - intro.
(* Goal: hypothesis_of_right_saccheri_quadrilaterals *)
    apply (per_sac__rah B A D C); auto.
(* Goal: @Per Tn B A D *)
    apply (t22_11__per _ _ _ C); auto.
(* Goal: @CongA Tn C A B A C D *)
    apply conga_left_comm.
(* Goal: @LtA Tn A C D B A C *)
    unfold Saccheri in HSac.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: @CongA Tn C A B A C D *)
    apply (sams2_suma2__conga456 B C A _ _ _ _ _ _ A B C); try (apply sams123231); auto.
(* Goal: @SAMS Tn B C A A C D *)
    { repeat split; auto.
(* Goal: False *)
(* Goal: False *)
      right; intro; assert_cols; Col.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Per Tn B C C') (@GtA Tn P Q R B C C')) *)
      exists D.
(* Goal: and (@CongA Tn A C D A C D) (and (not (@OS Tn C A B D)) (and (not (@TS Tn B C A D)) (@Coplanar Tn B C A D))) *)
      split; CongA; repeat split; Side; Cop.
    }
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Per Tn B C C') (@GtA Tn P Q R B C C')) *)
    exists D.
(* Goal: and (@CongA Tn A C D A C D) (and (not (@OS Tn C A B D)) (and (@Coplanar Tn B C A D) (@CongA Tn B C D A B C))) *)
    repeat (split; CongA); Side; Cop.

  - intro rah.
(* Goal: @SumA Tn B C A C A B A B C *)
    apply (conga3_suma__suma B C A A C D B C D); try (apply conga_refl); auto.
(* Goal: and (@CongA Tn A C D A C D) (and (not (@OS Tn C A B D)) (and (@Coplanar Tn B C A D) (@CongA Tn B C D A B C))) *)
      exists D; repeat (split; CongA); Side; Cop.
(* Goal: @CongA Tn A C D C A B *)
    apply conga_sym.
(* Goal: @CongA Tn C A B A C D *)
    apply conga_left_comm.
(* Goal: @CongA Tn B A C A C D *)
    apply t22_11__per; auto.
(* Goal: @Per Tn B A D *)
    apply (rah _ _ _ C); auto.
Qed.

Lemma t22_12__aah : forall A B C P Q R,
  Per A B C -> SumA B C A C A B P Q R ->
  (Acute P Q R <-> hypothesis_of_acute_saccheri_quadrilaterals).
Proof.
(* Goal: forall (A B C P Q R : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @SumA Tn B C A C A B P Q R), iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intros A B C P Q R HPer HSuma.
(* Goal: @LeA Tn D E F C A B' *)
  suma.assert_diffs.
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(~ Col A B C) by (apply per_not_col; auto).
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HD0 := l10_15 B C C A).
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  destruct HD0 as [D0 []]; Col.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HD := segment_construction_3 C D0 A B).
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  destruct HD as [D []]; auto.
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HSac : Saccheri B A D C).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { repeat split; Cong.
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
    apply (per_col _ _ D0); Col; Perp.
(* Goal: @OS Tn B C A D *)
    apply invert_one_side.
(* Goal: @OS Tn C B A D *)
    apply (out_out_one_side _ _ _ D0); Side.
  }
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  clear dependent D0.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.

(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HPars1 := sac__par_strict1423 B A D C HSac).
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HPars2 := sac__par_strict1234 B A D C HSac).
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(TS C A B D) by (apply l9_31; apply l12_6; Par).
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(CongA B C D A B C) by (unfold Saccheri in HSac; spliter; apply l11_16; auto).
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split.
  - intro.
(* Goal: hypothesis_of_acute_saccheri_quadrilaterals *)
    apply (acute_sac__aah B A D C); auto.
(* Goal: @Acute Tn B A D *)
    apply (t22_11__acute _ _ _ C); auto.
(* Goal: @LtA Tn A C D B A C *)
    unfold Saccheri in HSac.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: @LtA Tn B A C A C D *)
    apply lta_left_comm.
(* Goal: @LtA Tn C A B A C D *)
    apply (sams_lea_lta789_suma2__lta456 B C A _ _ _ P Q R B C A _ _ _ B C D); auto.
(* Goal: @LeA Tn B C A B C A *)
(* Goal: @LtA Tn A C D C A B *)
(* Goal: @SAMS Tn B C A C A B *)
(* Goal: @SumA Tn B C A A C D B C D *)
      apply lea_refl; auto.
(* Goal: @LtA Tn P Q R B C D *)
(* Goal: @SAMS Tn B C A C A B *)
(* Goal: @SumA Tn B C A A C D B C D *)
      apply acute_per__lta; auto.
(* Goal: @SAMS Tn D E F A C B *)
      SumA.
(* Goal: and (@CongA Tn A C D A C D) (and (not (@OS Tn C A B D)) (and (@Coplanar Tn B C A D) (@CongA Tn B C D A B C))) *)
      exists D; repeat (split; CongA); Side; Cop.

  - intro aah.
(* Goal: @SumA Tn A C M M C B A C B *)
    exists B.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Per Tn B B' C') (@GtA Tn P Q R B B' C'))) *)
    exists C.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Per Tn B C C') (@GtA Tn P Q R B C C')) *)
    exists D.
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
    split.
(* Goal: @Per Tn B C D *)
(* Goal: @GtA Tn P Q R B C D *)
      unfold Saccheri in HSac; spliter; auto.
(* Goal: @LtA Tn P Q R B C D *)
    apply (sams_lea_lta456_suma2__lta B C A C A B _ _ _ B C A A C D); auto.
(* Goal: @LeA Tn B C A B C A *)
(* Goal: @LtA Tn A C D C A B *)
(* Goal: @SAMS Tn B C A C A B *)
(* Goal: @SumA Tn B C A A C D B C D *)
      apply lea_refl; auto.
(* Goal: @LtA Tn C A B A C D *)
(* Goal: @SAMS Tn B C A A C D *)
(* Goal: @SumA Tn B C A A C D B C D *)
      apply lta_left_comm; apply t22_11__acute; try (apply (aah _ _ _ C)); auto.
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
      { split; auto; split.
(* Goal: False *)
(* Goal: False *)
          right; intro; assert_cols; Col.
(* Goal: and (@CongA Tn A' A B A' A B) (and (not (@OS Tn A A' C B)) (and (not (@TS Tn C A A' B)) (@Coplanar Tn C A A' B))) *)
        exists D; split; CongA.
(* Goal: and (not (@OS Tn C A B D)) (and (not (@TS Tn B C A D)) (@Coplanar Tn B C A D)) *)
        repeat split; Side; Cop.
      }
(* Goal: and (@CongA Tn A C D A C D) (and (not (@OS Tn C A B D)) (and (@Coplanar Tn B C A D) (@CongA Tn B C D A B C))) *)
      exists D; repeat (split; CongA); Side; Cop.
Qed.

Lemma t22_12__oah : forall A B C P Q R,
  Per A B C -> SumA B C A C A B P Q R ->
  (Obtuse P Q R <-> hypothesis_of_obtuse_saccheri_quadrilaterals).
Proof.
(* Goal: forall (A B C P Q R : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @SumA Tn B C A C A B P Q R), iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intros A B C P Q R HPer HSuma.
(* Goal: @LeA Tn D E F C A B' *)
  suma.assert_diffs.
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(~ Col A B C) by (apply per_not_col; auto).
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HD0 := l10_15 B C C A).
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  destruct HD0 as [D0 []]; Col.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HD := segment_construction_3 C D0 A B).
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  destruct HD as [D []]; auto.
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HSac : Saccheri B A D C).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { repeat split; Cong.
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
    apply (per_col _ _ D0); Col; Perp.
(* Goal: @OS Tn B C A D *)
    apply invert_one_side.
(* Goal: @OS Tn C B A D *)
    apply (out_out_one_side _ _ _ D0); Side.
  }
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  clear dependent D0.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.

(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HPars1 := sac__par_strict1423 B A D C HSac).
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HPars2 := sac__par_strict1234 B A D C HSac).
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(TS C A B D) by (apply l9_31; apply l12_6; Par).
(* Goal: iff (@Obtuse Tn P Q R) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(CongA B C D A B C) by (unfold Saccheri in HSac; spliter; apply l11_16; auto).
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split.
  - intro.
(* Goal: hypothesis_of_obtuse_saccheri_quadrilaterals *)
    apply (obtuse_sac__oah B A D C); auto.
(* Goal: @Obtuse Tn B A D *)
    apply (t22_11__obtuse _ _ _ C); auto.
(* Goal: @LtA Tn A C D B A C *)
    unfold Saccheri in HSac.
(* Goal: @LtA Tn A C D B A C *)
    spliter.
(* Goal: @LtA Tn A C D B A C *)
    apply lta_right_comm.
(* Goal: @LtA Tn A C D C A B *)
    apply (sams_lea_lta789_suma2__lta456 B C A _ _ _ B C D B C A _ _ _ P Q R); auto.
(* Goal: @LeA Tn B C A B C A *)
(* Goal: @LtA Tn A C D C A B *)
(* Goal: @SAMS Tn B C A C A B *)
(* Goal: @SumA Tn B C A A C D B C D *)
      apply lea_refl; auto.
(* Goal: @LtA Tn B C D P Q R *)
(* Goal: @SAMS Tn B C A A C D *)
(* Goal: @SumA Tn B C A A C D B C D *)
      apply obtuse_per__lta; auto.
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
      { split; auto; split.
(* Goal: False *)
(* Goal: False *)
        right; intro; assert_cols; Col.
(* Goal: and (@CongA Tn A' A B A' A B) (and (not (@OS Tn A A' C B)) (and (not (@TS Tn C A A' B)) (@Coplanar Tn C A A' B))) *)
        exists D; split; CongA.
(* Goal: and (not (@OS Tn C A B D)) (and (not (@TS Tn B C A D)) (@Coplanar Tn B C A D)) *)
        repeat split; Side; Cop.
      }
(* Goal: and (@CongA Tn A C D A C D) (and (not (@OS Tn C A B D)) (and (@Coplanar Tn B C A D) (@CongA Tn B C D A B C))) *)
      exists D; repeat (split; CongA); Side; Cop.

  - intro oah.
(* Goal: @SumA Tn A C M M C B A C B *)
    exists B.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Per Tn B B' C') (@GtA Tn P Q R B B' C'))) *)
    exists C.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Per Tn B C C') (@GtA Tn P Q R B C C')) *)
    exists D.
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
    split.
(* Goal: @Per Tn B C D *)
(* Goal: @GtA Tn P Q R B C D *)
      unfold Saccheri in HSac; spliter; auto.
(* Goal: @GtA Tn P Q R B C D *)
    apply (sams_lea_lta456_suma2__lta B C A A C D _ _ _ B C A C A B); auto.
(* Goal: @LeA Tn B C A B C A *)
(* Goal: @LtA Tn A C D C A B *)
(* Goal: @SAMS Tn B C A C A B *)
(* Goal: @SumA Tn B C A A C D B C D *)
      apply lea_refl; auto.
(* Goal: @LtA Tn A C D C A B *)
(* Goal: @SAMS Tn B C A C A B *)
(* Goal: @SumA Tn B C A A C D B C D *)
      apply lta_right_comm; apply t22_11__obtuse; try (apply (oah _ _ _ C)); auto.
(* Goal: @SAMS Tn D E F A C B *)
      SumA.
(* Goal: and (@CongA Tn A C D A C D) (and (not (@OS Tn C A B D)) (and (@Coplanar Tn B C A D) (@CongA Tn B C D A B C))) *)
      exists D; repeat (split; CongA); Side; Cop.
Qed.


Lemma t22_14__bet_aux : forall A B C P Q R,
  hypothesis_of_right_saccheri_quadrilaterals ->
  ~ Col A B C -> TriSumA A B C P Q R -> Acute A B C -> Acute A C B -> Bet P Q R.
Proof.
  intros A B C P Q R rah HNCol HTri HacuteB HacuteC.
(* Goal: hypothesis_of_right_saccheri_quadrilaterals *)
  apply trisuma_perm_312 in HTri.
(* Goal: False *)
  destruct HTri as [D [E [F []]]].

(* Goal: False *)
  assert(HA' := l8_18_existence B C A).
(* Goal: False *)
  destruct HA' as [A' []]; Col.
(* Goal: False *)
  assert(Out B A' C) by (apply (acute_col_perp__out A); auto).
(* Goal: False *)
  assert(Out C A' B) by (apply (acute_col_perp__out A); Col; Perp).
(* Goal: False *)
  assert(Bet B A' C) by (apply (out2__bet); [|apply l6_6]; auto).
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: False *)
  assert(Per B A' A) by (apply perp_per_1; auto; apply perp_left_comm; apply (perp_col _ C); Col).
(* Goal: False *)
  assert(Per C A' A) by (apply (l8_3 B); Col).
(* Goal: False *)
  assert(CongA B A' A C A' A) by (apply l11_16; auto).
(* Goal: False *)
  assert(CongA A B C A B A') by (apply (out_conga A B A' A B A'); try (apply out_trivial); CongA).
(* Goal: False *)
  assert(CongA B C A A' C A) by (apply (out_conga A' C A A' C A); try (apply out_trivial); CongA).
(* Goal: False *)
  assert(~ Col B A A') by (intro; apply HNCol; ColR).
(* Goal: False *)
  assert(~ Col C A A') by (intro; apply HNCol; ColR).
(* Goal: False *)
  assert(TS A A' B C) by (repeat split; try (exists A'); Col).

  apply (bet_conga__bet B A' C); auto.
  apply (suma2__conga D E F B C A); auto.
  apply (suma_assoc B A' A C A A' _ _ _ _ _ _ _ _ _ A A' C).
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
    apply (conga2_sams__sams C A' A A' A C); try (apply sams123231); CongA.
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
    apply (conga2_sams__sams A' A C A C A'); try (apply sams123231); CongA.
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { apply suma_sym.
(* Goal: @SumA Tn C A A' V W X D E F *)
      apply (suma_assoc _ _ _ A' A B A B C _ _ _ C A B); auto.
      - split; auto; split.
(* Goal: False *)
(* Goal: False *)
          right; intro; assert_cols; Col.
(* Goal: @SumA Tn A C M M C B A C B *)
        exists B.
(* Goal: and (@CongA Tn A' A B A' A B) (and (not (@OS Tn A A' C B)) (and (not (@TS Tn C A A' B)) (@Coplanar Tn C A A' B))) *)
        split; CongA.
(* Goal: and (@OS Tn D' A' B' C') (and (@CongA Tn B D A B' D' A') (@CongA Tn A D C A' D' C')) *)
        repeat split; Side.
(* Goal: not (@TS Tn C A A' B) *)
(* Goal: @Coplanar Tn C A A' B *)
          apply l9_9_bis; apply (out_one_side); Col.
(* Goal: and (@Col Tn I A D) (@Bet Tn B I C) *)
        exists C; left; split; Col.
      - apply (conga2_sams__sams A' A B A B A'); try (apply sams123231); CongA.
      - exists B; repeat (split; CongA); Side; exists C; left; split; Col.
      - apply (conga3_suma__suma A' A B A B A' B A' A); try (apply t22_12__rah); CongA.
    }
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
apply (conga3_suma__suma A' A C A C A' C A' A); try (apply t22_12__rah); CongA.
(* Goal: @SumA Tn B A' A A A' C B A' C *)
exists C; repeat (split; CongA); Side.
(* Goal: and (@Col Tn I A D) (@Bet Tn B I C) *)
exists C; left; split; Col.
Qed.

(** Under the Right angle hypothesis,
    the sum of the three angles of a triangle is equal to 180
 *)

Lemma t22_14__bet :
  hypothesis_of_right_saccheri_quadrilaterals ->
  forall A B C P Q R, TriSumA A B C P Q R -> Bet P Q R.
Proof.
(* Goal: forall (_ : hypothesis_of_right_saccheri_quadrilaterals) (A B C P Q R : @Tpoint Tn) (_ : @TriSumA Tn A B C P Q R), @Bet Tn P Q R *)
  intros rah A B C P Q R HTri.
(* Goal: @Bet Tn P Q R *)
  elim(col_dec A B C).
(* Goal: forall _ : @Col Tn A B C, @Bet Tn P Q R *)
(* Goal: forall _ : not (@Col Tn A B C), @Bet Tn P Q R *)
    intro; apply (col_trisuma__bet A B C); auto.
(* Goal: forall _ : @Obtuse Tn A C B, hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intro.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: not (@SAMS Tn D E F B C A) *)
  elim(angle_partition A B C); auto.
(* Goal: forall _ : @Acute Tn A B C, not (@SAMS Tn D E F B C A) *)
(* Goal: forall _ : or (@Per Tn A B C) (@Obtuse Tn A B C), not (@SAMS Tn D E F B C A) *)
  intro; elim(angle_partition A C B); auto.
  - intro.
(* Goal: @Bet Tn P Q R *)
    apply (t22_14__bet_aux A B C); auto.

  - intro.
(* Goal: not (@SAMS Tn D E F B C A) *)
    assert(HInter := l11_43 C A B).
(* Goal: not (@SAMS Tn D E F B C A) *)
    destruct HInter; Col.
(* Goal: @Bet Tn P Q R *)
    apply (t22_14__bet_aux C A B); Col.
(* Goal: @TriSumA Tn C A B P Q R *)
    apply trisuma_perm_312; auto.

  - intro.
(* Goal: not (@SAMS Tn D E F B C A) *)
    assert(HInter := l11_43 B A C).
(* Goal: not (@SAMS Tn D E F B C A) *)
    destruct HInter; Col.
(* Goal: @Bet Tn P Q R *)
    apply (t22_14__bet_aux B A C); Col.
(* Goal: @TriSumA Tn B A C P Q R *)
    apply trisuma_perm_213; auto.
Qed.


Lemma t22_14__sams_nbet_aux : forall A B C D E F P Q R,
  hypothesis_of_acute_saccheri_quadrilaterals ->
  ~ Col A B C ->
  SumA C A B A B C D E F -> SumA D E F B C A P Q R ->
  Acute A B C -> Acute A C B ->
  SAMS D E F B C A /\ ~ Bet P Q R.
Proof.
(* Goal: forall (A B C D E F P Q R : @Tpoint Tn) (_ : hypothesis_of_acute_saccheri_quadrilaterals) (_ : not (@Col Tn A B C)) (_ : @SumA Tn C A B A B C D E F) (_ : @SumA Tn D E F B C A P Q R) (_ : @Acute Tn A B C) (_ : @Acute Tn A C B), and (@SAMS Tn D E F B C A) (not (@Bet Tn P Q R)) *)
  intros A B C D E F P Q R aah HNCol HSuma1 HSuma2 HacuteB HacuteC.
(* Goal: False *)
  assert(HA' := l8_18_existence B C A).
(* Goal: False *)
  destruct HA' as [A' []]; Col.
(* Goal: False *)
  assert(Out B A' C) by (apply (acute_col_perp__out A); auto).
(* Goal: False *)
  assert(Out C A' B) by (apply (acute_col_perp__out A); Col; Perp).
(* Goal: False *)
  assert(Bet B A' C) by (apply (out2__bet); [|apply l6_6]; auto).
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: False *)
  assert(Per B A' A) by (apply perp_per_1; auto; apply perp_left_comm; apply (perp_col _ C); Col).
(* Goal: False *)
  assert(Per C A' A) by (apply (l8_3 B); Col).
(* Goal: False *)
  assert(CongA B A' A C A' A) by (apply l11_16; auto).
(* Goal: False *)
  assert(CongA A B C A B A') by (apply (out_conga A B A' A B A'); try (apply out_trivial); CongA).
(* Goal: False *)
  assert(CongA B C A A' C A) by (apply (out_conga A' C A A' C A); try (apply out_trivial); CongA).
(* Goal: False *)
  assert(~ Col B A A') by (intro; apply HNCol; ColR).
(* Goal: False *)
  assert(~ Col C A A') by (intro; apply HNCol; ColR).
(* Goal: False *)
  assert(TS A A' B C) by (repeat split; try (exists A'); Col).

(* Goal: @LtA Tn B A' C P Q R *)
  assert(HSuma3 := ex_suma B A' A C A A').
(* Goal: @LtA Tn B A' C P Q R *)
  rename H into HCol.
(* Goal: not (@SAMS Tn D E F B C A) *)
  destruct HSuma3 as [G [H [I HSuma3]]]; auto.
(* Goal: @LeA Tn D E F C A B' *)
  suma.assert_diffs.
(* Goal: and (@SAMS Tn D E F B C A) (not (@Bet Tn P Q R)) *)
  assert(LtA D E F G H I).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { assert(HSuma4 := ex_suma A' A B A B C).
(* Goal: @LtA Tn G H I D E F *)
    destruct HSuma4 as [V [W [X HSuma4]]]; auto.
(* Goal: @LeA Tn D E F C A B' *)
    suma.assert_diffs.
(* Goal: @LtA Tn D E F G H I *)
    apply (sams_lea_lta456_suma2__lta C A A' V W X _ _ _ C A A' B A' A); Lea.
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
      apply (acute_per__lta); auto; apply (t22_12__aah B A' A); auto; apply (conga3_suma__suma A' A B A B C V W X); CongA.
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
      apply (conga2_sams__sams C A A' A A' C); SumA; CongA.
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
      { apply (suma_assoc _ _ _ A' A B A B C _ _ _ C A B); auto.
        - split; auto; split.
(* Goal: False *)
(* Goal: False *)
            right; intro; assert_cols; Col.
(* Goal: @SumA Tn A C M M C B A C B *)
          exists B.
(* Goal: and (@CongA Tn A' A B A' A B) (and (not (@OS Tn A A' C B)) (and (not (@TS Tn C A A' B)) (@Coplanar Tn C A A' B))) *)
          split; CongA.
(* Goal: and (@OS Tn D' A' B' C') (and (@CongA Tn B D A B' D' A') (@CongA Tn A D C A' D' C')) *)
          repeat split; Side.
(* Goal: not (@TS Tn C A A' B) *)
(* Goal: @Coplanar Tn C A A' B *)
            apply l9_9_bis; apply (out_one_side); Col.
(* Goal: and (@Col Tn I A D) (@Bet Tn B I C) *)
          exists C; left; split; Col.
        - apply (conga2_sams__sams A' A B A B A'); SumA; CongA.
        - exists B; repeat (split; CongA); Side.
(* Goal: and (@Col Tn I A D) (@Bet Tn B I C) *)
          exists C; left; split; Col.
      }
(* Goal: @SumA Tn C A A' B A' A G H I *)
      apply suma_sym; auto.
  }
(* Goal: @LtA Tn B A' C P Q R *)
  assert(HSuma4 := ex_suma C A A' B C A).
(* Goal: @LtA Tn B A' C P Q R *)
  destruct HSuma4 as [J [K [L HSuma4]]]; auto.
(* Goal: @LeA Tn D E F C A B' *)
  suma.assert_diffs.
(* Goal: and (@SAMS Tn D E F B C A) (not (@Bet Tn P Q R)) *)
  assert(LtA J K L A A' C).
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
    apply (acute_per__lta); Perp; apply (t22_12__aah C A' A); auto; apply (conga3_suma__suma C A A' B C A J K L); CongA.
(* Goal: and (@SAMS Tn D E F B C A) (not (@Bet Tn P Q R)) *)
  assert(SAMS G H I B C A).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { apply (sams_assoc B A' A C A A' _ _ _ _ _ _ J K L); auto.
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
      apply (conga2_sams__sams C A' A A' A C); SumA; CongA.
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
      apply (conga2_sams__sams A' A C A C A'); SumA; CongA.
(* Goal: @SAMS Tn B A' A A A' C *)
      apply (sams_chara _ _ _ _ _ _ C); Lea.
  }
(* Goal: and (@SAMS Tn D E F B C A) (not (@Bet Tn P Q R)) *)
  assert(HSuma5 := ex_suma G H I B C A).
(* Goal: @LtA Tn B A' C P Q R *)
  destruct HSuma5 as [S [T [U HSuma5]]]; auto.
(* Goal: @LeA Tn D E F C A B' *)
  suma.assert_diffs.
(* Goal: and (@SAMS Tn D E F B C A) (not (@Bet Tn P Q R)) *)
  assert(LtA S T U B A' C).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { apply (sams_lea_lta456_suma2__lta B A' A J K L _ _ _ B A' A A A' C); Lea.
    - apply (sams_chara _ _ _ _ _ _ C); Lea.
    - apply (suma_assoc _ _ _ C A A' B C A _ _ _ G H I); auto;
      [apply (conga2_sams__sams C A' A A' A C)|apply (conga2_sams__sams A' A C A C A')];
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
      SumA; CongA.
    - exists C; repeat(split; CongA); Side.
(* Goal: and (@Col Tn I A D) (@Bet Tn B I C) *)
      exists C; left; split; Col.
  }

(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split.
(* Goal: @SAMS Tn D E F B C A *)
(* Goal: not (@Bet Tn P Q R) *)
    apply (sams_lea2__sams _ _ _ _ _ _ G H I B C A); Lea.
(* Goal: forall _ : @Obtuse Tn A C B, hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intro.
(* Goal: False *)
  apply (nlta P Q R).
(* Goal: @LtA Tn P Q R P Q R *)
  apply (conga_preserves_lta P Q R B A' C).
(* Goal: @CongA Tn P Q R P Q R *)
(* Goal: @CongA Tn B A' C P Q R *)
(* Goal: @LtA Tn P Q R B A' C *)
    apply conga_refl; auto.
(* Goal: @CongA Tn B A' C P Q R *)
(* Goal: @LtA Tn P Q R B A' C *)
    apply conga_line; auto.
(* Goal: @LtA Tn P Q R B A' C *)
  apply (lta_trans _ _ _ S T U); auto.
(* Goal: @LtA Tn P Q R S T U *)
  apply (sams_lea_lta123_suma2__lta D E F B C A _ _ _ G H I B C A); Lea.
Qed.

(** Under the Acute angle hypothesis,
    the sum of the three angles of a triangle is less than 180
 *)

Lemma t22_14__sams_nbet :
  hypothesis_of_acute_saccheri_quadrilaterals ->
  forall A B C D E F P Q R, ~ Col A B C ->
  SumA C A B A B C D E F -> SumA D E F B C A P Q R ->
  SAMS D E F B C A /\ ~ Bet P Q R.
Proof.
(* Goal: forall (_ : hypothesis_of_acute_saccheri_quadrilaterals) (A B C D E F P Q R : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @SumA Tn C A B A B C D E F) (_ : @SumA Tn D E F B C A P Q R), and (@SAMS Tn D E F B C A) (not (@Bet Tn P Q R)) *)
  intros aah A B C D E F P Q R HNCol HSuma1 HSuma2.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: not (@SAMS Tn D E F B C A) *)
  elim(angle_partition A B C); auto.
(* Goal: forall _ : @Acute Tn A B C, not (@SAMS Tn D E F B C A) *)
(* Goal: forall _ : or (@Per Tn A B C) (@Obtuse Tn A B C), not (@SAMS Tn D E F B C A) *)
  intro; elim(angle_partition A C B); auto.
  - intro.
(* Goal: and (@SAMS Tn D E F B C A) (not (@Bet Tn P Q R)) *)
    apply (t22_14__sams_nbet_aux A B C); auto.

  - intro.
(* Goal: not (@SAMS Tn D E F B C A) *)
    assert(HInter := l11_43 C A B).
(* Goal: not (@SAMS Tn D E F B C A) *)
    destruct HInter; Col.
(* Goal: not (@SAMS Tn D E F B C A) *)
    assert(HSuma3 := ex_suma B C A C A B).
(* Goal: not (@SAMS Tn D E F B C A) *)
    rename H into HAcute.
(* Goal: not (@SAMS Tn D E F B C A) *)
    destruct HSuma3 as [G [H [I HSuma3]]]; auto.
(* Goal: @LeA Tn D E F C A B' *)
    suma.assert_diffs.
(* Goal: and (@SAMS Tn D E F B C A) (not (@Bet Tn P Q R)) *)
    assert(HInter := t22_14__sams_nbet_aux C A B G H I P Q R).
(* Goal: and (@SAMS Tn D E F B C A) (not (@Bet Tn P Q R)) *)
    destruct HInter as [HIsi HNBet]; Col.
(* Goal: @SAMS Tn D E F A C B *)
      apply (suma_assoc B C A C A B _ _ _ _ _ _ _ _ _ D E F); SumA.
(* Goal: and (@SumA Tn C A B A B C D E F) (@SumA Tn D E F B C A D E D') *)
    split; auto.
(* Goal: @SAMS Tn D E F A C B *)
    apply sams_sym; apply (sams_assoc _ _ _ C A B A B C G H I); SumA.

  - intro.
(* Goal: not (@SAMS Tn D E F B C A) *)
    assert (HInter := l11_43 B A C).
(* Goal: not (@SAMS Tn D E F B C A) *)
    destruct HInter; Col.
(* Goal: and (@SAMS Tn D E F B C A) (not (@Bet Tn P Q R)) *)
    assert(HInter := t22_14__sams_nbet_aux B A C D E F P Q R).
(* Goal: @SAMS Tn D E F A C B *)
    destruct HInter as [HIsi HNBet]; Col; SumA.
Qed.

Lemma t22_14__nsams_aux : forall A B C D E F,
  hypothesis_of_obtuse_saccheri_quadrilaterals ->
  ~ Col A B C ->
  SumA C A B A B C D E F -> Acute A B C -> Acute A C B ->
  ~ SAMS D E F B C A.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : hypothesis_of_obtuse_saccheri_quadrilaterals) (_ : not (@Col Tn A B C)) (_ : @SumA Tn C A B A B C D E F) (_ : @Acute Tn A B C) (_ : @Acute Tn A C B), not (@SAMS Tn D E F B C A) *)
  intros A B C D E F oah HNCol HSuma1 HacuteB HacuteC HIsi.
(* Goal: False *)
  assert(HA' := l8_18_existence B C A).
(* Goal: False *)
  destruct HA' as [A' []]; Col.
(* Goal: False *)
  assert(Out B A' C) by (apply (acute_col_perp__out A); auto).
(* Goal: False *)
  assert(Out C A' B) by (apply (acute_col_perp__out A); Col; Perp).
(* Goal: False *)
  assert(Bet B A' C) by (apply (out2__bet); [|apply l6_6]; auto).
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: False *)
  assert(Per B A' A) by (apply perp_per_1; auto; apply perp_left_comm; apply (perp_col _ C); Col).
(* Goal: False *)
  assert(Per C A' A) by (apply (l8_3 B); Col).
(* Goal: False *)
  assert(CongA B A' A C A' A) by (apply l11_16; auto).
(* Goal: False *)
  assert(CongA A B C A B A') by (apply (out_conga A B A' A B A'); try (apply out_trivial); CongA).
(* Goal: False *)
  assert(CongA B C A A' C A) by (apply (out_conga A' C A A' C A); try (apply out_trivial); CongA).
(* Goal: False *)
  assert(~ Col B A A') by (intro; apply HNCol; ColR).
(* Goal: False *)
  assert(~ Col C A A') by (intro; apply HNCol; ColR).
(* Goal: False *)
  assert(TS A A' B C) by (repeat split; try (exists A'); Col).

(* Goal: False *)
  assert(HSuma2 := ex_suma D E F B C A).
(* Goal: False *)
  destruct HSuma2 as [P [Q [R HSuma2]]]; suma.assert_diffs; auto.
(* Goal: False *)
  absurd (LtA B A' C P Q R).
(* Goal: @LeA Tn R S T B P C *)
(* Goal: @LtA Tn B P C R S T *)
    apply (lea__nlta); apply l11_31_2; auto.
(* Goal: @LtA Tn B A' C P Q R *)
  assert(HSuma3 := ex_suma B A' A C A A').
(* Goal: @LtA Tn B A' C P Q R *)
  rename H into HCol.
(* Goal: not (@SAMS Tn D E F B C A) *)
  destruct HSuma3 as [G [H [I HSuma3]]]; auto.
(* Goal: @LtA Tn B A' C P Q R *)
  assert(LtA G H I D E F).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { assert(HSuma4 := ex_suma A' A B A B C).
(* Goal: @LtA Tn G H I D E F *)
    destruct HSuma4 as [V [W [X HSuma4]]]; auto.
(* Goal: @LeA Tn D E F C A B' *)
    suma.assert_diffs.
(* Goal: @LtA Tn G H I D E F *)
    assert(SAMS C A A' A' A B).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { split; auto; split.
(* Goal: False *)
(* Goal: False *)
      right; intro; assert_cols; Col.
(* Goal: @SumA Tn A C M M C B A C B *)
      exists B.
(* Goal: and (@CongA Tn A' A B A' A B) (and (not (@OS Tn A A' C B)) (and (not (@TS Tn C A A' B)) (@Coplanar Tn C A A' B))) *)
      repeat (split; CongA); Side.
(* Goal: @OS Tn B J R C *)
        apply l9_9_bis; apply out_one_side; Col.
(* Goal: and (@Col Tn I A D) (@Bet Tn B I C) *)
      exists C; left; split; Col.
    }
(* Goal: @LtA Tn G H I D E F *)
    assert(SAMS A' A B A B C) by (apply (conga2_sams__sams A' A B A B A'); SumA; CongA).
(* Goal: @LtA Tn G H I D E F *)
    assert(SumA C A A' A' A B C A B) by (exists B; repeat (split; CongA); Side; Cop).
(* Goal: @LtA Tn G H I D E F *)
    apply (sams_lea_lta456_suma2__lta C A A' B A' A _ _ _ C A A' V W X); Lea.
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
      apply (obtuse_per__lta); auto; apply (t22_12__oah B A' A); auto; apply (conga3_suma__suma A' A B A B C V W X); CongA.
(* Goal: @SAMS Tn D E F A C B *)
      apply (sams_assoc _ _ _ A' A B A B C C A B); SumA.
(* Goal: @SAMS Tn D E F A C B *)
      SumA.
(* Goal: @SumA Tn C A A' V W X D E F *)
      apply (suma_assoc _ _ _ A' A B A B C _ _ _ C A B); auto.
  }
(* Goal: @LtA Tn B A' C P Q R *)
  assert(HSuma4 := ex_suma C A A' B C A).
(* Goal: @LtA Tn B A' C P Q R *)
  destruct HSuma4 as [J [K [L HSuma4]]]; auto.
(* Goal: @LeA Tn D E F C A B' *)
  suma.assert_diffs.
(* Goal: @LtA Tn B A' C P Q R *)
  assert(LtA A A' C J K L).
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
    apply (obtuse_per__lta); Perp; apply (t22_12__oah C A' A); auto; apply (conga3_suma__suma C A A' B C A J K L); CongA.
(* Goal: @LtA Tn B A' C P Q R *)
  assert(HSuma5 := ex_suma B A' A J K L).
(* Goal: @LtA Tn B A' C P Q R *)
  destruct HSuma5 as [S [T [U HSuma5]]]; auto.
(* Goal: @LeA Tn D E F C A B' *)
  suma.assert_diffs.
(* Goal: @LtA Tn B A' C P Q R *)
  apply (lta_trans _ _ _ S T U).
  - apply (sams_lea_lta456_suma2__lta B A' A A A' C _ _ _ B A' A J K L); Lea;
    [|exists C; repeat (split; CongA); Side; Cop].
(* Goal: @SAMS Tn B A' A J K L *)
    apply (sams_assoc _ _ _ C A A' B C A G H I); auto.
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
      apply (conga2_sams__sams C A' A C A A'); SumA; CongA.
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
      apply (conga2_sams__sams C A A' A' C A); SumA; CongA.
(* Goal: @SAMS Tn G H I B C A *)
    apply (sams_lea2__sams _ _ _ _ _ _ D E F B C A); Lea.

  - apply (sams_lea_lta123_suma2__lta G H I B C A _ _ _ D E F B C A); Lea.
(* Goal: @SumA Tn G H I B C A S T U *)
    apply (suma_assoc B A' A C A A' _ _ _ _ _ _ _ _ _ J K L); auto.
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
      apply (conga2_sams__sams C A' A C A A'); SumA; CongA.
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
      apply (conga2_sams__sams C A A' A' C A); SumA; CongA.
Qed.

(** Under the Obtuse angle hypothesis,
    the sum of the three angles of a triangle is greater than 180
 *)

Lemma t22_14__nsams :
  hypothesis_of_obtuse_saccheri_quadrilaterals ->
  forall A B C D E F, ~ Col A B C ->
  SumA C A B A B C D E F ->
  ~ SAMS D E F B C A.
Proof.
(* Goal: forall (_ : hypothesis_of_obtuse_saccheri_quadrilaterals) (A B C D E F : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @SumA Tn C A B A B C D E F), not (@SAMS Tn D E F B C A) *)
  intros oah A B C D E F HNCol HSuma1.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: not (@SAMS Tn D E F B C A) *)
  elim(angle_partition A B C); auto.
(* Goal: forall _ : @Acute Tn A B C, not (@SAMS Tn D E F B C A) *)
(* Goal: forall _ : or (@Per Tn A B C) (@Obtuse Tn A B C), not (@SAMS Tn D E F B C A) *)
  intro; elim(angle_partition A C B); auto.
  - intro.
(* Goal: not (@SAMS Tn D E F B C A) *)
    apply (t22_14__nsams_aux A B C); auto.

  - intro.
(* Goal: not (@SAMS Tn D E F B C A) *)
    assert(HInter := l11_43 C A B).
(* Goal: not (@SAMS Tn D E F B C A) *)
    destruct HInter; Col.
(* Goal: not (@SAMS Tn D E F B C A) *)
    assert(HSuma3 := ex_suma B C A C A B).
(* Goal: not (@SAMS Tn D E F B C A) *)
    rename H into HAcute.
(* Goal: not (@SAMS Tn D E F B C A) *)
    destruct HSuma3 as [G [H [I HSuma3]]]; auto.
(* Goal: @LeA Tn D E F C A B' *)
    suma.assert_diffs.
(* Goal: not (@SAMS Tn D E F B C A) *)
    assert(HNIsi := t22_14__nsams_aux C A B G H I).
(* Goal: not (@SAMS Tn D E F B C A) *)
    intro HIsi.
(* Goal: False *)
    absurd(SAMS G H I A B C).
(* Goal: not (@SAMS Tn G H I A B C) *)
(* Goal: @SAMS Tn G H I A B C *)
      apply HNIsi; Col.
(* Goal: @SAMS Tn D E F A C B *)
      apply (sams_assoc B C A C A B _ _ _ _ _ _ D E F); SumA.

  - intro.
(* Goal: not (@SAMS Tn D E F B C A) *)
    assert (HInter := l11_43 B A C).
(* Goal: not (@SAMS Tn D E F B C A) *)
    destruct HInter; Col.
(* Goal: forall _ : @Obtuse Tn A C B, hypothesis_of_obtuse_saccheri_quadrilaterals *)
    intro.
(* Goal: False *)
    absurd(SAMS D E F A C B).
(* Goal: @SAMS Tn D E F A C B *)
      apply (t22_14__nsams_aux B A C D E F); Col; SumA.
(* Goal: @SAMS Tn D E F A C B *)
      SumA.
Qed.


(** If the sum of the angles of a non-degenerate triangle is equal to 180,
    then the Right angle hypothesis holds
 *)

Lemma t22_14__rah : forall A B C P Q R,
  ~ Col A B C -> TriSumA A B C P Q R -> Bet P Q R -> hypothesis_of_right_saccheri_quadrilaterals.
Proof.
(* Goal: forall (A B C P Q R : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @TriSumA Tn A B C P Q R) (_ : @Bet Tn P Q R), hypothesis_of_right_saccheri_quadrilaterals *)
  intros A B C P Q R HNCol HTri HBet.
(* Goal: hypothesis_of_right_saccheri_quadrilaterals *)
  apply trisuma_perm_312 in HTri.
(* Goal: hypothesis_of_obtuse_saccheri_quadrilaterals *)
  destruct (saccheri_s_three_hypotheses) as [aah|[rah|oah]]; auto; exfalso.
  - destruct HTri as [D [E [F []]]].
(* Goal: False *)
    assert(HInter := t22_14__sams_nbet aah A B C D E F P Q R).
(* Goal: False *)
    destruct HInter; auto.

  - exfalso.
(* Goal: False *)
    destruct HTri as [D [E [F [HSuma1 HSuma2]]]].
(* Goal: False *)
    apply (t22_14__nsams oah A B C D E F); auto.
(* Goal: @SAMS Tn D E F B C A *)
    destruct HSuma2 as [G [HConga1 [HNos [HCop HConga2]]]].
(* Goal: @SAMS Tn D E F B C A *)
    apply conga_sym in HConga1.
(* Goal: @LeA Tn D E F C A B' *)
    assert_diffs.
(* Goal: @SAMS Tn D E F B C A *)
    apply (sams_chara _ _ _ _ _ _ G); Lea.
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
    apply (bet_conga__bet P Q R); CongA.
Qed.

(** If the sum of the angles of a triangle is less than 180,
    then the Acute angle hypothesis holds
 *)

Lemma t22_14__aah : forall A B C D E F P Q R,
  SumA C A B A B C D E F -> SumA D E F B C A P Q R ->
  SAMS D E F B C A ->
  ~ Bet P Q R ->
  hypothesis_of_acute_saccheri_quadrilaterals.
Proof.
(* Goal: forall (A B C D E F P Q R : @Tpoint Tn) (_ : @SumA Tn C A B A B C D E F) (_ : @SumA Tn D E F B C A P Q R) (_ : @SAMS Tn D E F B C A) (_ : not (@Bet Tn P Q R)), hypothesis_of_acute_saccheri_quadrilaterals *)
  intros A B C D E F P Q R HSuma1 HSuma2 HIsi HNBet.
(* Goal: hypothesis_of_obtuse_saccheri_quadrilaterals *)
  destruct(saccheri_s_three_hypotheses) as [|[rah|oah]]; auto; exfalso.
  - apply HNBet.
(* Goal: @Bet Tn P Q R *)
    apply (t22_14__bet rah A B C).
(* Goal: @TriSumA Tn A B C P Q R *)
    apply trisuma_perm_231.
(* Goal: @TriSumA Tn C A B D E D' *)
    exists D; exists E; exists F.
(* Goal: and (@SumA Tn C A B A B C D E F) (@SumA Tn D E F B C A D E D') *)
    split; auto.

  - destruct (col_dec A B C).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
    { apply HNBet.
(* Goal: @Bet Tn P Q R *)
      apply (col_trisuma__bet C A B); Col.
(* Goal: @TriSumA Tn C A B D E D' *)
      exists D; exists E; exists F.
(* Goal: and (@SumA Tn C A B A B C D E F) (@SumA Tn D E F B C A D E D') *)
      split; auto.
    }
(* Goal: False *)
    absurd(SAMS D E F B C A); auto.
(* Goal: not (@SAMS Tn D E F B C A) *)
    apply t22_14__nsams; auto.
Qed.

(** If the sum of the angles of a triangle is greater than 180,
    then the Obtuse angle hypothesis holds
 *)

Lemma t22_14__oah : forall A B C D E F,
  SumA C A B A B C D E F -> ~ SAMS D E F B C A -> hypothesis_of_obtuse_saccheri_quadrilaterals.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @SumA Tn C A B A B C D E F) (_ : not (@SAMS Tn D E F B C A)), hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intros A B C D E F HSuma1 HNIsi.
(* Goal: hypothesis_of_obtuse_saccheri_quadrilaterals *)
  destruct(col_dec A B C).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { exfalso.
(* Goal: False *)
    apply HNIsi.
(* Goal: @LeA Tn D E F C A B' *)
    suma.assert_diffs.
(* Goal: @SAMS Tn D E F B C A *)
    elim(bet_dec A B C).
    - intro.
(* Goal: @SAMS Tn D E F A C B *)
      apply (conga2_sams__sams A B C B C A); try (apply conga_refl); SumA.
(* Goal: @CongA Tn A B C D E F *)
      apply (out213_suma__conga C A B); auto.
(* Goal: @Out Tn S R I *)
      apply l6_6; apply bet_out; auto.

    - intro.
(* Goal: @SAMS Tn D E F A C B *)
      apply (conga2_sams__sams C A B B C A); try (apply conga_refl); SumA.
(* Goal: @CongA Tn C A B D E F *)
      apply (out546_suma__conga _ _ _ A B C); auto.
(* Goal: @Out Tn B A C *)
      apply not_bet_out; auto.
  }
(* Goal: @LeA Tn D E F C A B' *)
  destruct (saccheri_s_three_hypotheses) as [aah|[rah|oah]]; auto; exfalso; suma.assert_diffs.
  - assert(HSuma2 := ex_suma D E F B C A).
(* Goal: False *)
    destruct HSuma2 as [P [Q [R HSuma2]]]; auto.
(* Goal: False *)
    assert(HInter := t22_14__sams_nbet aah A B C D E F P Q R).
(* Goal: False *)
    destruct HInter; auto.

  - apply HNIsi.
(* Goal: @SAMS Tn D E F B C A *)
    assert(~ Col D E F) by (apply (ncol_suma__ncol C A B); Col).
(* Goal: @SAMS Tn D E F B C A *)
    assert(HD' := ex_conga_ts B C A F E D).
(* Goal: @SAMS Tn D E F B C A *)
    destruct HD' as [D' []]; Col.
(* Goal: @LeA Tn D E F C A B' *)
    suma.assert_diffs.
(* Goal: @SAMS Tn D E F B C A *)
    apply (sams_chara _ _ _ _ _ _ D'); Lea.
(* Goal: @Bet Tn P Q R *)
    apply (t22_14__bet rah C A B).
(* Goal: @TriSumA Tn C A B D E D' *)
    exists D; exists E; exists F.
(* Goal: and (@SumA Tn C A B A B C D E F) (@SumA Tn D E F B C A D E D') *)
    split; auto.
(* Goal: and (@CongA Tn A C D A C D) (and (not (@OS Tn C A B D)) (and (@Coplanar Tn B C A D) (@CongA Tn B C D A B C))) *)
    exists D'; repeat (split; CongA); Side; Cop.
Qed.


(** If C is on the circle of diameter AB, then we have the angles equation A + B = C *)

Lemma cong_mid__suma : forall A B C M,
  ~ Col A B C ->
  Midpoint M A B -> Cong M A M C ->
  SumA C A B A B C A C B.
Proof.
(* Goal: forall (A B C M : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Midpoint Tn M A B) (_ : @Cong Tn M A M C), iff (@Acute Tn A C B) hypothesis_of_acute_saccheri_quadrilaterals *)
  intros A B C M HNCol HM HCong.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @SumA Tn C A B A B C A C B *)
  assert(CongA A B C M C B).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { apply (out_conga M B C M C B); try (apply out_trivial); auto;
    [|apply bet_out; Between].
(* Goal: @CongA Tn M B C M C B *)
    apply l11_44_1_a; auto.
(* Goal: @Cong Tn M B M C *)
    apply (cong_transitivity _ _ M A); Cong.
  }
(* Goal: @SumA Tn C A B A B C A C B *)
  assert(CongA B A C M C A).
(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
  { apply (out_conga M A C M C A); try (apply out_trivial); auto;
    [|apply bet_out; Between].
(* Goal: @CongA Tn M A C M C A *)
    apply l11_44_1_a; Cong.
  }
(* Goal: @CongA Tn P N M P' N' M' *)
(* Goal: @CongA Tn M P Q M' P' Q' *)
  apply (conga3_suma__suma A C M M C B A C B); CongA.
(* Goal: @SumA Tn A C M M C B A C B *)
  exists B.
(* Goal: and (@CongA Tn M C B M C B) (and (not (@OS Tn C M A B)) (and (@Coplanar Tn A C M B) (@CongA Tn A C B A C B))) *)
  repeat (split; CongA); [|exists A; left; split; Col].
(* Goal: not (@OS Tn C M A B) *)
  apply l9_9.
(* Goal: @TS Tn C M A B *)
  repeat split; auto; try (intro; apply HNCol; ColR).
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T C M) (@Bet Tn A T B)) *)
  exists M.
(* Goal: and (@Col Tn M C M) (@Bet Tn A M B) *)
  split; Col; Between.
Qed.


(** The three following lemmas link Saccheri's three hypotheses
    with triangles ABC having C on the circle of diameter AB;
    the first one states the equivalence between the Right angle hypothesis and Thales' theorem
 *)

Lemma t22_17__rah : forall A B C M,
  ~ Col A B C ->
  Midpoint M A B -> Cong M A M C ->
  (Per A C B <-> hypothesis_of_right_saccheri_quadrilaterals).
Proof.
(* Goal: forall (A B C M : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Midpoint Tn M A B) (_ : @Cong Tn M A M C), iff (@Acute Tn A C B) hypothesis_of_acute_saccheri_quadrilaterals *)
  intros A B C M HNCol HM HCong.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(SumA C A B A B C A C B) by (apply (cong_mid__suma _ _ _ M); auto).
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HSuma := ex_suma A C B B C A).
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  destruct HSuma as [P [Q [R]]]; auto.
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split.
  - intro.
(* Goal: hypothesis_of_right_saccheri_quadrilaterals *)
    apply (t22_14__rah C A B P Q R); Col.
(* Goal: @TriSumA Tn C A B P Q R *)
      exists A; exists C; exists B; auto.
(* Goal: @Perp Tn C D N D *)
(* Goal: @Col Tn C D H *)
(* Goal: @Perp Tn C D N H *)
      apply (per2_suma__bet A C B B C A); Perp.

  - intro rah.
(* Goal: @SAMS Tn D E F A C B *)
    apply (bet_suma__per _ _ _ P Q R); SumA.
(* Goal: @Bet Tn P Q R *)
    apply (t22_14__bet rah C A B).
(* Goal: @TriSumA Tn C A B P Q R *)
    exists A; exists C; exists B; auto.
Qed.

Lemma t22_17__oah : forall A B C M,
  ~ Col A B C ->
  Midpoint M A B -> Cong M A M C ->
  (Obtuse A C B <-> hypothesis_of_obtuse_saccheri_quadrilaterals).
Proof.
(* Goal: forall (A B C M : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Midpoint Tn M A B) (_ : @Cong Tn M A M C), iff (@Acute Tn A C B) hypothesis_of_acute_saccheri_quadrilaterals *)
  intros A B C M HNCol HM HCong.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(SumA C A B A B C A C B) by (apply (cong_mid__suma _ _ _ M); auto).
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  assert(HSuma := ex_suma A C B B C A).
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  destruct HSuma as [P [Q [R]]]; auto.
(* Goal: iff (@Obtuse Tn A C B) hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split.
  - intro.
(* Goal: @SAMS Tn D E F A C B *)
    apply (t22_14__oah A B C B C A); Col; SumA.
(* Goal: not (@SAMS Tn B C A B C A) *)
    apply obtuse__nsams; apply obtuse_sym; auto.

  - intro oah.
(* Goal: @Obtuse Tn A C B *)
    apply obtuse_sym.
(* Goal: @Obtuse Tn B C A *)
    apply nsams__obtuse; auto.
(* Goal: @SAMS Tn D E F A C B *)
    apply (t22_14__nsams oah A B C); Col; SumA.
Qed.

Lemma t22_17__aah : forall A B C M,
  ~ Col A B C ->
  Midpoint M A B -> Cong M A M C ->
  (Acute A C B <-> hypothesis_of_acute_saccheri_quadrilaterals).
Proof.
(* Goal: forall (A B C M : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Midpoint Tn M A B) (_ : @Cong Tn M A M C), iff (@Acute Tn A C B) hypothesis_of_acute_saccheri_quadrilaterals *)
  intros A B C M HNCol HM HCong.
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: forall _ : @Obtuse Tn A C B, hypothesis_of_obtuse_saccheri_quadrilaterals *)
  split; intro.
  - destruct (saccheri_s_three_hypotheses) as [|[rah|oah]]; auto; exfalso; apply (nlta A C B).
(* Goal: @LtA Tn A C B A C B *)
(* Goal: @LtA Tn A C B A C B *)
      apply (acute_per__lta); auto; rewrite (t22_17__rah _ _ _ M); auto.
(* Goal: @LtA Tn A C B A C B *)
      apply (acute_obtuse__lta); auto; rewrite (t22_17__oah _ _ _ M); auto.

  - destruct (angle_partition A C B) as [|[|]]; auto;
    absurd(hypothesis_of_acute_saccheri_quadrilaterals); auto; apply not_aah.
(* Goal: or hypothesis_of_right_saccheri_quadrilaterals hypothesis_of_obtuse_saccheri_quadrilaterals *)
(* Goal: or hypothesis_of_right_saccheri_quadrilaterals hypothesis_of_obtuse_saccheri_quadrilaterals *)
      left; apply (t22_17__rah A B C M); auto.
(* Goal: or hypothesis_of_right_saccheri_quadrilaterals hypothesis_of_obtuse_saccheri_quadrilaterals *)
      right; apply (t22_17__oah A B C M); auto.
Qed.

Lemma t22_20 : ~ hypothesis_of_obtuse_saccheri_quadrilaterals ->
  forall A B C D E F, SumA A B C B C A D E F -> SAMS D E F C A B.
Proof.
(* Goal: forall (_ : not hypothesis_of_obtuse_saccheri_quadrilaterals) (A B C D E F : @Tpoint Tn) (_ : @SumA Tn A B C B C A D E F), @SAMS Tn D E F C A B *)
  intros noah A B C D E F HS.
(* Goal: @SAMS Tn D E F C A B *)
  elim(sams_dec D E F C A B); trivial.
(* Goal: hypothesis_of_obtuse_saccheri_quadrilaterals *)
  intro HNI; exfalso.
(* Goal: False *)
  apply noah, (t22_14__oah B C A D E F); trivial.
Qed.

Lemma absolute_exterior_angle_theorem : ~ hypothesis_of_obtuse_saccheri_quadrilaterals ->
  forall A B C D E F B', Bet B A B' -> A <> B' -> SumA A B C B C A D E F ->
  LeA D E F C A B'.
Proof.
(* Goal: forall (_ : not hypothesis_of_obtuse_saccheri_quadrilaterals) (A B C D E F B' : @Tpoint Tn) (_ : @Bet Tn B A B') (_ : not (@eq (@Tpoint Tn) A B')) (_ : @SumA Tn A B C B C A D E F), @LeA Tn D E F C A B' *)
  intros noah A B C D E F B' HBet HAB' HSuma.
(* Goal: @LeA Tn D E F C A B' *)
  assert (HIsi := t22_20 noah A B C D E F HSuma).
(* Goal: @LeA Tn D E F C A B' *)
  assert_diffs.
(* Goal: @SAMS Tn D E F A C B *)
  apply sams_chara with B; SumA.
Qed.

End Saccheri.

Hint Resolve sac__par_strict1423 sac__par_strict1234 sac__par1423 sac__par1234
lam__par_strict1234 lam__par_strict1423 lam__par1234 lam__par1423 : Par.

Hint Resolve sac__coplanar : cop.

Section Saccheri_2D.

(* Goal: @CongA Tn B A C M C A *)
(* Goal: @SumA Tn C A B A B C A C B *)
Context `{T2D:Tarski_2D}.

Lemma sac2__sac : forall A B C D E F,
  Saccheri A B C D -> Saccheri A B E F -> D <> F -> Saccheri D C E F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @Saccheri Tn A B C D) (_ : @Saccheri Tn A B E F) (_ : not (@eq (@Tpoint Tn) D F)), @Saccheri Tn D C E F *)
  intros A B C D E F H1 H2 HDF.
(* Goal: @Saccheri Tn D C E F *)
  assert (HCop := all_coplanar A B D F).
(* Goal: @Saccheri Tn D C E F *)
  apply (cop_sac2__sac A B); assumption.
Qed.

End Saccheri_2D.