Require Export GeoCoq.Tarski_dev.Annexes.saccheri.

Section Defect.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma defect_distincts : forall A B C D E F,
  Defect A B C D E F ->
  A <> B /\ B <> C /\ A <> C /\ D <> E /\ E <> F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @Defect Tn A B C D E F), @Defect Tn C B A D E F *)
  intros A B C D E F HDef.
(* Goal: @hypothesis_of_right_saccheri_quadrilaterals Tn *)
  destruct HDef as [G [H [I [HTri HSuppa]]]].
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  suma.assert_diffs.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) B C)) (and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) D E)) (not (@eq (@Tpoint Tn) E F))))) *)
  repeat split; auto.
Qed.

Lemma ex_defect : forall A B C,
  A <> B -> B <> C -> A <> C -> exists D E F, Defect A B C D E F.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) B C)) (_ : not (@eq (@Tpoint Tn) A C)), @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => @ex (@Tpoint Tn) (fun F : @Tpoint Tn => @Defect Tn A B C D E F))) *)
  intros A B C HAB HBC HAC.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => @ex (@Tpoint Tn) (fun F : @Tpoint Tn => @Defect Tn A B C D E F))) *)
  destruct (ex_trisuma A B C) as [G [H [I HTri]]]; auto.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  suma.assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => @ex (@Tpoint Tn) (fun F : @Tpoint Tn => @Defect Tn A B C D E F))) *)
  destruct (ex_suppa G H I) as [D [E [F HSuppa]]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => @ex (@Tpoint Tn) (fun F : @Tpoint Tn => @Defect Tn A B C D E F))) *)
  exists D, E, F, G, H, I.
(* Goal: and (@TriSumA Tn A B C G H I) (@SuppA Tn G H I D E F) *)
  split; assumption.
Qed.

Lemma conga_defect__defect : forall A B C D E F D' E' F',
  Defect A B C D E F -> CongA D E F D' E' F' ->
  Defect A B C D' E' F'.
Proof.
(* Goal: forall (A B C D E F D' E' F' : @Tpoint Tn) (_ : @Defect Tn A B C D E F) (_ : @CongA Tn D E F D' E' F'), @Defect Tn A B C D' E' F' *)
  intros A B C D E F D' E' F' HDef HConga.
(* Goal: @hypothesis_of_right_saccheri_quadrilaterals Tn *)
  destruct HDef as [G [H [I [HTri HSuppa]]]].
(* Goal: @Defect Tn A' B' C' D E F *)
  exists G, H, I.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  split; trivial.
(* Goal: @SuppA Tn G H I D' E' F' *)
  assert_diffs.
(* Goal: @SuppA Tn G H I D' E' F' *)
  apply (conga2_suppa__suppa G H I D E F); CongA.
Qed.

Lemma defect2__conga : forall A B C D E F D' E' F',
  Defect A B C D E F -> Defect A B C D' E' F' ->
  CongA D E F D' E' F'.
Proof.
(* Goal: forall (A B C D E F D' E' F' : @Tpoint Tn) (_ : @Defect Tn A B C D E F) (_ : @Defect Tn A B C D' E' F'), @CongA Tn D E F D' E' F' *)
  intros A B C D E F D' E' F' HDef HDef'.
(* Goal: @hypothesis_of_right_saccheri_quadrilaterals Tn *)
  destruct HDef as [G [H [I [HTri HSuppa]]]].
(* Goal: @CongA Tn D E F D' E' F' *)
  destruct HDef' as [G' [H' [I' [HTri' HSuppa']]]].
(* Goal: @CongA Tn D E F D' E' F' *)
  apply (suppa2__conga456 G H I); trivial.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  suma.assert_diffs.
(* Goal: @SuppA Tn G H I D' E' F' *)
  apply (conga2_suppa__suppa G' H' I' D' E' F'); try apply conga_refl; auto.
(* Goal: @CongA Tn G' H' I' G H I *)
  apply (trisuma2__conga A B C); assumption.
Qed.

Lemma defect_perm_231 : forall A B C D E F,
  Defect A B C D E F -> Defect B C A D E F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @Defect Tn A B C D E F), @Defect Tn C B A D E F *)
  intros A B C D E F HDef.
(* Goal: @hypothesis_of_right_saccheri_quadrilaterals Tn *)
  destruct HDef as [G [H [I [HTri HSuppa]]]].
(* Goal: @Defect Tn A' B' C' D E F *)
  exists G, H, I.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  split; trivial.
(* Goal: @TriSumA Tn B C A G H I *)
  apply trisuma_perm_231, HTri.
Qed.

Lemma defect_perm_312 : forall A B C D E F,
  Defect A B C D E F -> Defect C A B D E F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @Defect Tn A B C D E F), @Defect Tn A C B D E F *)
  intros.
(* Goal: @Defect Tn C A B D E F *)
  do 2 apply defect_perm_231; trivial.
Qed.

Lemma defect_perm_321 : forall A B C D E F,
  Defect A B C D E F -> Defect C B A D E F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @Defect Tn A B C D E F), @Defect Tn C B A D E F *)
  intros A B C D E F HDef.
(* Goal: @hypothesis_of_right_saccheri_quadrilaterals Tn *)
  destruct HDef as [G [H [I [HTri HSuppa]]]].
(* Goal: @Defect Tn A' B' C' D E F *)
  exists G, H, I.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  split; trivial.
(* Goal: @TriSumA Tn C B A G H I *)
  apply trisuma_perm_321, HTri.
Qed.

Lemma defect_perm_213 : forall A B C D E F,
  Defect A B C D E F -> Defect B A C D E F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @Defect Tn A B C D E F), @Defect Tn A C B D E F *)
  intros.
(* Goal: @Defect Tn B A C D E F *)
  apply defect_perm_321, defect_perm_312; trivial.
Qed.

Lemma defect_perm_132 : forall A B C D E F,
  Defect A B C D E F -> Defect A C B D E F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @Defect Tn A B C D E F), @Defect Tn A C B D E F *)
  intros.
(* Goal: @Defect Tn A C B D E F *)
  apply defect_perm_321, defect_perm_231; trivial.
Qed.

Lemma conga3_defect__defect : forall A B C D E F A' B' C',
  Defect A B C D E F ->
  CongA A B C A' B' C' -> CongA B C A B' C' A' -> CongA C A B C' A' B' ->
  Defect A' B' C' D E F.
Proof.
(* Goal: forall (A B C D E F A' B' C' : @Tpoint Tn) (_ : @Defect Tn A B C D E F) (_ : @CongA Tn A B C A' B' C') (_ : @CongA Tn B C A B' C' A') (_ : @CongA Tn C A B C' A' B'), @Defect Tn A' B' C' D E F *)
  intros A B C D E F A' B' C' HDef HCongaB HCongaC HCongaA.
(* Goal: @hypothesis_of_right_saccheri_quadrilaterals Tn *)
  destruct HDef as [G [H [I [HTri HSuppa]]]].
(* Goal: @Defect Tn A' B' C' D E F *)
  exists G, H, I.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  split; trivial.
(* Goal: @TriSumA Tn A' B' C' G H I *)
  apply (conga3_trisuma__trisuma A B C); trivial.
Qed.

Lemma col_defect__out : forall A B C D E F,
  Col A B C -> Defect A B C D E F -> Out E D F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @Col Tn A B C) (_ : @Defect Tn A B C D E F), @Out Tn E D F *)
  intros A B C D E F HCol HDef.
(* Goal: @hypothesis_of_right_saccheri_quadrilaterals Tn *)
  destruct HDef as [G [H [I [HTri HSuppa]]]].
(* Goal: @Out Tn E D F *)
  apply (bet_suppa__out G H I); trivial.
(* Goal: @Bet Tn G H I *)
  apply (col_trisuma__bet A B C); Col.
Qed.

Lemma rah_defect__out :
  hypothesis_of_right_saccheri_quadrilaterals ->
  forall A B C D E F, Defect A B C D E F -> Out E D F.
Proof.
(* Goal: forall (_ : @hypothesis_of_right_saccheri_quadrilaterals Tn) (A B C D E F : @Tpoint Tn) (_ : @Defect Tn A B C D E F), @Out Tn E D F *)
  intros rah A B C D E F HDef.
(* Goal: @hypothesis_of_right_saccheri_quadrilaterals Tn *)
  destruct HDef as [G [H [I [HTri HSuppa]]]].
(* Goal: @Out Tn E D F *)
  apply (bet_suppa__out G H I); trivial.
(* Goal: @Bet Tn G H I *)
  apply (t22_14__bet rah A B C), HTri.
Qed.

Lemma defect_ncol_out__rah : forall A B C D E F,
  ~ Col A B C -> Defect A B C D E F -> Out E D F ->
  hypothesis_of_right_saccheri_quadrilaterals.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Defect Tn A B C D E F) (_ : @Out Tn E D F), @hypothesis_of_right_saccheri_quadrilaterals Tn *)
  intros A B C D E F HNCol HDef HOut.
(* Goal: @hypothesis_of_right_saccheri_quadrilaterals Tn *)
  destruct HDef as [G [H [I [HTri HSuppa]]]].
(* Goal: @hypothesis_of_right_saccheri_quadrilaterals Tn *)
  apply (t22_14__rah A B C G H I); trivial.
(* Goal: @Bet Tn G H I *)
  apply (out_suppa__bet D E F); [|apply suppa_sym]; assumption.
Qed.

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

(** Additivity of the defect : if C1 is between A and C, the defect of ABC is
    the sum of the defects of ABC1 and BC1C.
    In this proof, we have to exclude the semi-elliptical case so that the sums of angles behave. *)
Lemma t22_16_1 :
  ~ hypothesis_of_obtuse_saccheri_quadrilaterals ->
  forall A B C C1 D E F G H I K L M,
    Bet A C1 C -> Defect A B C1 D E F -> Defect B C1 C G H I ->
    SumA D E F G H I K L M ->
    SAMS D E F G H I /\ Defect A B C K L M.
Proof.
(* Goal: forall (_ : not (@hypothesis_of_obtuse_saccheri_quadrilaterals Tn)) (A B C C1 D E F G H I K L M : @Tpoint Tn) (_ : @Bet Tn A C1 C) (_ : @Defect Tn A B C1 D E F) (_ : @Defect Tn B C1 C G H I) (_ : @SumA Tn D E F G H I K L M), and (@SAMS Tn D E F G H I) (@Defect Tn A B C K L M) *)
  intros noah A B C C1 D E F G H I K L M HBet HDefA HDefC HSuma.
(* Goal: and (@SAMS Tn D E F G H I) (@Defect Tn A B C K L M) *)
  assert (HDA := defect_distincts A B C1 D E F HDefA).
(* Goal: and (@SAMS Tn D E F G H I) (@Defect Tn A B C K L M) *)
  assert (HDC := defect_distincts B C1 C G H I HDefC).
(* Goal: and (@SAMS Tn D E F G H I) (@Defect Tn A B C K L M) *)
  spliter; clean.
(* Goal: and (@SAMS Tn D E F G H I) (@Defect Tn A B C K L M) *)
  apply defect_perm_321 in HDefA.
(* Goal: and (@SAMS Tn D E F G H I) (@Defect Tn A B C K L M) *)
  destruct HDefA as [P [Q [R [HTri HSuppa]]]].
(* Goal: and (@SAMS Tn D E F G H I) (@Defect Tn A B C K L M) *)
  assert (HSuma1 : SumA P Q R D E F A C1 C) by SumA.
(* Goal: and (@SAMS Tn D E F G H I) (@Defect Tn A B C K L M) *)
  destruct HTri as [S [T [U [HSuma2 HSuma3]]]].
(* Goal: and (@SAMS Tn D E F G H I) (@Defect Tn A B C K L M) *)
  assert (HInter : SumA S T U D E F B C1 C /\ SAMS S T U D E F).
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  { suma.assert_diffs.
(* Goal: and (@SumA Tn S T U D E F B C1 C) (@SAMS Tn S T U D E F) *)
    destruct (ex_suma S T U D E F) as [B' [C1' [C' HSuma']]]; auto.
(* Goal: and (@SumA Tn S T U D E F B C1 C) (@SAMS Tn S T U D E F) *)
    assert (HSuma4 : SumA B C1 C A C1 B A C1 C) by (apply suma_sym, inangle__suma, in_angle_line; auto).
(* Goal: and (@SumA Tn S T U D E F B C1 C) (@SAMS Tn S T U D E F) *)
    destruct (ex_suma A C1 B D E F) as [V [W [X HSuma5]]]; auto.
(* Goal: and (@SumA Tn S T U D E F B C1 C) (@SAMS Tn S T U D E F) *)
    assert (HIsi : SAMS P Q R D E F) by (apply bet_suma__sams with A C1 C; trivial).
(* Goal: and (@SumA Tn S T U D E F B C1 C) (@SAMS Tn S T U D E F) *)
    assert (HIsi1 : SAMS S T U A C1 B) by (apply (t22_20 noah), HSuma2).
(* Goal: and (@SumA Tn S T U D E F B C1 C) (@SAMS Tn S T U D E F) *)
    assert (HIsi2 : SAMS A C1 B D E F).
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    { apply sams_lea2__sams with P Q R D E F; Lea.
(* Goal: @LeA Tn D E F B C1 C *)
(* Goal: @LeA Tn B C1 C P Q R *)
      apply (sams_suma__lea456789 S T U); trivial.
    }
(* Goal: and (@SumA Tn S T U D E F B C1 C) (@SAMS Tn S T U D E F) *)
    assert (HSuma6 : SumA S T U V W X A C1 C) by (apply suma_assoc_1 with A C1 B D E F P Q R; trivial).
(* Goal: and (@SumA Tn S T U D E F B C1 C) (@SAMS Tn S T U D E F) *)
    assert (HIsi3 : SAMS S T U D E F).
(* Goal: @SAMS Tn S T U D E F *)
(* Goal: and (@SumA Tn S T U D E F B C1 C) (@SAMS Tn S T U D E F) *)
      apply sams_lea2__sams with P Q R D E F; Lea; apply sams_suma__lea123789 with A C1 B; SumA.
(* Goal: and (@SumA Tn S T U D E F B C1 C) (@SAMS Tn S T U D E F) *)
    assert (HSuma7 : SumA B' C1' C' A C1 B A C1 C) by (apply suma_assoc_2 with S T U D E F V W X; SumA).
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    split; trivial.
(* Goal: @SumA Tn S T U D E F B C1 C *)
    apply (conga3_suma__suma S T U D E F B' C1' C'); try (apply conga_refl); auto.
(* Goal: @CongA Tn B' C1' C' B C1 C *)
    apply sams2_suma2__conga123 with A C1 B A C1 C; trivial; apply bet_suma__sams with A C1 C; trivial.
  }
(* Goal: and (@SAMS Tn D E F G H I) (@Defect Tn A B C K L M) *)
  clear dependent P; clear Q R.

(* Goal: and (@SAMS Tn D E F G H I) (@Defect Tn A B C K L M) *)
  destruct HInter as [HSuma3 HIsi3].
(* Goal: and (@SAMS Tn D E F G H I) (@Defect Tn A B C K L M) *)
  apply defect_perm_231 in HDefC.
(* Goal: and (@SAMS Tn D E F G H I) (@Defect Tn A B C K L M) *)
  destruct HDefC as [P [Q [R [HTri HSuppa]]]].
(* Goal: and (@SAMS Tn D E F G H I) (@Defect Tn A B C K L M) *)
  assert (HSuma1 : SumA P Q R G H I A C1 C) by SumA.
(* Goal: and (@SAMS Tn D E F G H I) (@Defect Tn A B C K L M) *)
  destruct HTri as [V [W [X [HSuma4 HSuma5]]]].
(* Goal: and (@SAMS Tn D E F G H I) (@Defect Tn A B C K L M) *)
  assert (HIsi1 : SAMS P Q R G H I) by (apply bet_suma__sams with A C1 C; trivial).
(* Goal: and (@SAMS Tn D E F G H I) (@Defect Tn A B C K L M) *)
  assert (HIsi5 : SAMS V W X B C1 C) by (apply (t22_20 noah), HSuma4).
(* Goal: and (@SAMS Tn D E F G H I) (@Defect Tn A B C K L M) *)
  assert (HIsi : SAMS D E F G H I).
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  { apply sams_lea2__sams with P Q R G H I; Lea.
(* Goal: @LeA Tn D E F P Q R *)
    apply lea_trans with B C1 C.
(* Goal: @LeA Tn D E F B C1 C *)
(* Goal: @LeA Tn B C1 C P Q R *)
      apply (sams_suma__lea456789 S T U); trivial.
(* Goal: @LeA Tn B C1 C P Q R *)
    apply (sams_suma__lea456789 V W X); trivial.
  }
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  split; trivial.

(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  suma.assert_diffs.
(* Goal: @Defect Tn A B C K L M *)
  destruct (ex_suma V W X S T U) as [A' [B' [C' HSuma6]]]; auto.
(* Goal: @Defect Tn A B C K L M *)
  assert (HIsi6 : SAMS V W X S T U).
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  { apply sams_lea2__sams with V W X B C1 C; Lea.
(* Goal: @LeA Tn S T U B C1 C *)
    apply sams_suma__lea123789 with D E F; trivial.
  }
(* Goal: @Defect Tn A B C K L M *)
  assert (HSuma7 : SumA A' B' C' D E F P Q R) by (apply suma_assoc_2 with V W X S T U B C1 C; trivial).
(* Goal: @Defect Tn A B C K L M *)
  assert (HSuma8 : SumA A' B' C' K L M A C1 C).
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  { apply suma_assoc_1 with D E F G H I P Q R; trivial.
(* Goal: @SAMS Tn A' B' C' D E F *)
    apply sams_assoc_2 with V W X S T U B C1 C; trivial.
  }
(* Goal: @Defect Tn A B C K L M *)
  exists A', B', C'.
(* Goal: and (@TriSumA Tn A B C A' B' C') (@SuppA Tn A' B' C' K L M) *)
  split; [|apply bet_suma__suppa with A C1 C; assumption].
  clear dependent D; clear dependent E; clear dependent G; clear dependent H;
  clear dependent K; clear dependent L; clear dependent P; clear dependent Q; clear F I M R.

(* Goal: @TriSumA Tn A B C A' B' C' *)
  destruct (ex_suma V W X C1 B A) as [D [E [F HSuma]]]; auto.
(* Goal: @TriSumA Tn A B C A' B' C' *)
  assert (HIsi : SAMS V W X C1 B A).
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  { apply sams_lea2__sams with V W X S T U; Lea.
(* Goal: @LeA Tn C1 B A S T U *)
    apply sams_suma__lea123789 with B A C1; SumA.
  }
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  suma.assert_diffs.
(* Goal: @TriSumA Tn A B C A' B' C' *)
  apply trisuma_perm_132.
(* Goal: @TriSumA Tn A C B A' B' C' *)
  exists D; exists E; exists F.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  split.
  - assert (HConga : CongA C1 C B A C B).
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    { apply (out_conga C1 C B C1 C B); try (apply out_trivial); CongA.
(* Goal: @Out Tn C C1 A *)
      apply bet_out; Between.
    }
(* Goal: @SumA Tn A C B C B A D E F *)
    apply (conga3_suma__suma C1 C B C B A D E F); CongA.
(* Goal: @SumA Tn C1 C B C B A D E F *)
    assert (HInAngle : InAngle C1 C B A).
(* Goal: @InAngle Tn C1 C B A *)
(* Goal: @SumA Tn C1 C B C B A D E F *)
      repeat split; auto; exists C1; split; Between; right; apply out_trivial; auto.
(* Goal: @SumA Tn C1 C B C B A D E F *)
    apply suma_assoc_1 with C B C1 C1 B A V W X; SumA.
  - assert (HConga : CongA B A C B A C1).
(* Goal: @CongA Tn B A C B A C1 *)
(* Goal: @SumA Tn D E F B A C A' B' C' *)
      apply (out_conga B A C1 B A C1); try (apply out_trivial); CongA; apply bet_out; auto.
(* Goal: @SumA Tn D E F B A C A' B' C' *)
    apply (conga3_suma__suma D E F B A C1 A' B' C'); CongA.
(* Goal: @SumA Tn D E F B A C1 A' B' C' *)
    apply suma_assoc_2 with V W X C1 B A S T U; SumA.
Qed.

Lemma t22_16_1bis :
  ~ hypothesis_of_obtuse_saccheri_quadrilaterals ->
  forall A B C C1 D E F G H I K L M,
    Bet A C1 C ->
    Defect A B C1 D E F -> Defect B C1 C G H I -> Defect A B C K L M ->
    SAMS D E F G H I /\ SumA D E F G H I K L M.
Proof.
(* Goal: forall (_ : not (@hypothesis_of_obtuse_saccheri_quadrilaterals Tn)) (A B C C1 D E F G H I K L M : @Tpoint Tn) (_ : @Bet Tn A C1 C) (_ : @Defect Tn A B C1 D E F) (_ : @Defect Tn B C1 C G H I) (_ : @Defect Tn A B C K L M), and (@SAMS Tn D E F G H I) (@SumA Tn D E F G H I K L M) *)
  intros noah A B C C1 D E F G H I K L M HBet HDefA HDefB HDef.
(* Goal: and (@SAMS Tn D E F G H I) (@SumA Tn D E F G H I K L M) *)
  assert (Hd := defect_distincts A B C1 D E F HDefA).
(* Goal: and (@SAMS Tn D E F G H I) (@SumA Tn D E F G H I K L M) *)
  assert (Hd' := defect_distincts B C1 C G H I HDefB).
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  spliter.
(* Goal: and (@SAMS Tn D E F G H I) (@SumA Tn D E F G H I K L M) *)
  destruct (ex_suma D E F G H I) as [K' [L' [M' HSuma]]]; auto.
(* Goal: and (@SAMS Tn D E F G H I) (@SumA Tn D E F G H I K L M) *)
  destruct (t22_16_1 noah A B C C1 D E F G H I K' L' M') as [HIsi HDef']; trivial.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  split; trivial.
(* Goal: @SumA Tn D E F G H I K L M *)
  apply (conga3_suma__suma D E F G H I K' L' M'); try (apply conga_refl); auto.
(* Goal: @CongA Tn K' L' M' K L M *)
  apply (defect2__conga A B C); trivial.
Qed.


Lemma t22_16_2aux :
  ~ hypothesis_of_obtuse_saccheri_quadrilaterals ->
  forall A B C D A1 A2 A3 B1 B2 B3 C1 C2 C3 D1 D2 D3 O P Q R,
    Defect A B C D1 D2 D3 -> Defect A B D C1 C2 C3 ->
    Defect A D C B1 B2 B3 -> Defect C B D A1 A2 A3 ->
    Bet A O C -> Bet B O D -> Col A B C -> SumA D1 D2 D3 B1 B2 B3 P Q R ->
    SAMS C1 C2 C3 A1 A2 A3 /\ SumA C1 C2 C3 A1 A2 A3 P Q R.
Proof.
  intros noah A B C D A1 A2 A3 B1 B2 B3 C1 C2 C3 D1 D2 D3 O P Q R
    HDefD HDefC HDefB HDefA HBet HBet2 HCol HSuma.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  assert (Hd := defect_distincts A B D C1 C2 C3 HDefC).
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  assert (Hd' := defect_distincts C B D A1 A2 A3 HDefA).
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  assert (Hd'' := defect_distincts A B C D1 D2 D3 HDefD).
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  spliter; suma.assert_diffs.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  apply col_defect__out in HDefD; trivial.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  destruct (col_dec A D C) as [HCol1|HNCol].
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  { assert (Col C B D) by ColR.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    assert (Col A B D) by ColR.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    apply col_defect__out in HDefA; trivial.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    apply col_defect__out in HDefB; trivial.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    apply col_defect__out in HDefC; trivial.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    split; [SumA|].
    apply (conga3_suma__suma D1 D2 D3 B1 B2 B3 P Q R); try (apply conga_refl); auto;
    apply l11_21_b; trivial.
  }
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  assert (B = O) by (apply (l6_21 A C D B); Col).
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  subst O.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  apply out213_suma__conga in HSuma; trivial.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  destruct (t22_16_1bis noah A D C B C1 C2 C3 A1 A2 A3 B1 B2 B3) as [HIsi HSuma1]; trivial.
(* Goal: @Defect Tn A D B C1 C2 C3 *)
(* Goal: @Defect Tn D B C A1 A2 A3 *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    apply defect_perm_132, HDefC.
(* Goal: @Defect Tn D B C A1 A2 A3 *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    apply defect_perm_321, HDefA.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  split; trivial.
(* Goal: @SumA Tn C1 C2 C3 A1 A2 A3 P Q R *)
  apply (conga3_suma__suma C1 C2 C3 A1 A2 A3 B1 B2 B3); CongA.
Qed.

Lemma t22_16_2aux1 :
  ~ hypothesis_of_obtuse_saccheri_quadrilaterals ->
  forall A B C D A1 A2 A3 B1 B2 B3 C1 C2 C3 D1 D2 D3 O P Q R,
    Defect A B C D1 D2 D3 -> Defect A B D C1 C2 C3 ->
    Defect A D C B1 B2 B3 -> Defect C B D A1 A2 A3 ->
    Bet A O C -> Bet B O D -> Col A B D -> SumA D1 D2 D3 B1 B2 B3 P Q R ->
    SAMS C1 C2 C3 A1 A2 A3 /\ SumA C1 C2 C3 A1 A2 A3 P Q R.
Proof.
  intros noah A B C D A1 A2 A3 B1 B2 B3 C1 C2 C3 D1 D2 D3 O P Q R
    HDefD HDefC HDefB HDefA HBet HBet2 HCol HSuma.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  assert (Hd := defect_distincts A B D C1 C2 C3 HDefC).
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  assert (Hd' := defect_distincts C B D A1 A2 A3 HDefA).
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  spliter; suma.assert_diffs.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  assert (HOut : Out C2 C1 C3) by (apply (col_defect__out A B D); trivial).
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  split; [SumA|].
(* Goal: @SumA Tn C1 C2 C3 A1 A2 A3 P Q R *)
  assert (HSuma1 : SumA C1 C2 C3 A1 A2 A3 A1 A2 A3) by (apply out213__suma; auto).
(* Goal: @SumA Tn C1 C2 C3 A1 A2 A3 P Q R *)
  apply (conga3_suma__suma C1 C2 C3 A1 A2 A3 A1 A2 A3); try (apply conga_refl); auto.
(* Goal: @CongA Tn A1 A2 A3 P Q R *)
  apply (suma2__conga D1 D2 D3 B1 B2 B3); trivial.
  destruct (t22_16_2aux noah B A D C B1 B2 B3 A1 A2 A3 D1 D2 D3 C1 C2 C3 O A1 A2 A3); Col;
  apply defect_perm_213; trivial.
Qed.

(** In a convex quadrilateral ABCD, the sum of the defects of ABC and ADC is equal to
    the sum of the defects of ABD and CBD. We add some hypotheses to make the proof easier *)
Lemma t22_16_2 :
  ~ hypothesis_of_obtuse_saccheri_quadrilaterals ->
  forall A B C D A1 A2 A3 B1 B2 B3 C1 C2 C3 D1 D2 D3 O P Q R,
    Defect A B C D1 D2 D3 -> Defect A B D C1 C2 C3 ->
    Defect A D C B1 B2 B3 -> Defect C B D A1 A2 A3 ->
    Bet A O C -> Bet B O D ->
    SAMS D1 D2 D3 B1 B2 B3 -> SumA D1 D2 D3 B1 B2 B3 P Q R ->
    SAMS C1 C2 C3 A1 A2 A3 /\ SumA C1 C2 C3 A1 A2 A3 P Q R.
Proof.
  intros noah A B C D A1 A2 A3 B1 B2 B3 C1 C2 C3 D1 D2 D3 O P Q R
    HDefD HDefC HDefB HDefA HBet HBet2 HIsi HSuma.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  assert (Hd := defect_distincts A B D C1 C2 C3 HDefC).
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  assert (Hd' := defect_distincts C B D A1 A2 A3 HDefA).
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  spliter; suma.assert_diffs.

(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  destruct (col_dec A B C) as [HCol|HNCol].
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    apply (t22_16_2aux noah A B C D A1 A2 A3 B1 B2 B3 C1 C2 C3 D1 D2 D3 O); trivial.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  destruct (col_dec A D C) as [HCol1|HNCol1].
    apply (t22_16_2aux noah A D C B A1 A2 A3 D1 D2 D3 C1 C2 C3 B1 B2 B3 O); Between; SumA;
    apply defect_perm_132; trivial.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  destruct (col_dec A B D) as [HCol2|HNCol2].
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    apply (t22_16_2aux1 noah A B C D A1 A2 A3 B1 B2 B3 C1 C2 C3 D1 D2 D3 O); trivial.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  destruct (col_dec C B D) as [HCol3|HNCol3].
    destruct (t22_16_2aux1 noah C B A D C1 C2 C3 B1 B2 B3 A1 A2 A3 D1 D2 D3 O P Q R); Between; SumA;
    apply defect_perm_321; trivial.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  assert (Hdiff : O <> A /\ O <> B /\ O <> C /\ O <> D).
(* Goal: and (not (@eq (@Tpoint Tn) O A)) (and (not (@eq (@Tpoint Tn) O B)) (and (not (@eq (@Tpoint Tn) O C)) (not (@eq (@Tpoint Tn) O D)))) *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    assert_cols; repeat split; intro; subst O; Col.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  spliter.

(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  destruct (ex_defect A B O) as [S1 [T1 [U1 HDef1]]]; auto.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  destruct (ex_defect B C O) as [S2 [T2 [U2 HDef2]]]; auto.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  destruct (ex_defect C D O) as [S3 [T3 [U3 HDef3]]]; auto.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  destruct (ex_defect A D O) as [S4 [T4 [U4 HDef4]]]; auto.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  destruct (t22_16_1bis noah A B C O S1 T1 U1 S2 T2 U2 D1 D2 D3) as [HIsi12 HSuma12]; trivial.
(* Goal: @Defect Tn B O C S2 T2 U2 *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    apply defect_perm_132, HDef2.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  destruct (t22_16_1bis noah A D C O S4 T4 U4 S3 T3 U3 B1 B2 B3) as [HIsi34 HSuma34]; trivial.
(* Goal: @Defect Tn D O C S3 T3 U3 *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    apply defect_perm_231, HDef3.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  destruct (t22_16_1bis noah B A D O S1 T1 U1 S4 T4 U4 C1 C2 C3) as [HIsi14 HSuma14]; trivial.
(* Goal: @Defect Tn B A O S1 T1 U1 *)
(* Goal: @Defect Tn A O D S4 T4 U4 *)
(* Goal: @Defect Tn B A D C1 C2 C3 *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    apply defect_perm_213, HDef1.
(* Goal: @Defect Tn A O D S4 T4 U4 *)
(* Goal: @Defect Tn B A D C1 C2 C3 *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    apply defect_perm_132, HDef4.
(* Goal: @Defect Tn B A D C1 C2 C3 *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    apply defect_perm_213, HDefC.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  destruct (t22_16_1bis noah B C D O S2 T2 U2 S3 T3 U3 A1 A2 A3) as [HIsi23 HSuma23]; trivial.
(* Goal: @Defect Tn C O D S3 T3 U3 *)
(* Goal: @Defect Tn B C D A1 A2 A3 *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    apply defect_perm_132, HDef3.
(* Goal: @Defect Tn B C D A1 A2 A3 *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    apply defect_perm_213, HDefA.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  suma.assert_diffs.

(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  destruct (ex_suma D1 D2 D3 S3 T3 U3) as [V [W [X HSuma1]]]; auto.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  assert (HIsi1 : SAMS D1 D2 D3 S3 T3 U3).
(* Goal: @SAMS Tn D1 D2 D3 S3 T3 U3 *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    apply sams_lea2__sams with D1 D2 D3 B1 B2 B3; Lea; apply (sams_suma__lea456789 S4 T4 U4); trivial.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  assert (HSuma2 : SumA V W X S4 T4 U4 P Q R).
(* Goal: @SumA Tn V W X S4 T4 U4 P Q R *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    apply suma_assoc_2 with D1 D2 D3 S3 T3 U3 B1 B2 B3; SumA.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  assert (HIsi2 : SAMS V W X S4 T4 U4).
(* Goal: @SAMS Tn V W X S4 T4 U4 *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    apply sams_assoc_2 with D1 D2 D3 S3 T3 U3 B1 B2 B3; SumA.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  assert (HSuma3 : SumA A1 A2 A3 S1 T1 U1 V W X).
(* Goal: @SumA Tn A1 A2 A3 S1 T1 U1 V W X *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    apply suma_assoc_2 with S3 T3 U3 S2 T2 U2 D1 D2 D3; SumA.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  assert (HIsi3 : SAMS A1 A2 A3 S1 T1 U1).
(* Goal: @SAMS Tn A1 A2 A3 S1 T1 U1 *)
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
    apply sams_assoc_2 with S3 T3 U3 S2 T2 U2 D1 D2 D3; SumA.
(* Goal: and (@SAMS Tn C1 C2 C3 A1 A2 A3) (@SumA Tn C1 C2 C3 A1 A2 A3 P Q R) *)
  split.
(* Goal: @SAMS Tn C1 C2 C3 A1 A2 A3 *)
(* Goal: @SumA Tn C1 C2 C3 A1 A2 A3 P Q R *)
    apply sams_assoc_2 with S4 T4 U4 S1 T1 U1 V W X; SumA.
(* Goal: @SumA Tn C1 C2 C3 A1 A2 A3 P Q R *)
  apply suma_assoc_2 with S4 T4 U4 S1 T1 U1 V W X; SumA.
Qed.

End Defect.