proposition: 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: 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. assert (Hd := defect_distincts A B D C1 C2 C3 HDefC). assert (Hd' := defect_distincts C B D A1 A2 A3 HDefA). spliter; suma.assert_diffs. destruct (col_dec A B C) as [HCol|HNCol]. apply (t22_16_2aux noah A B C D A1 A2 A3 B1 B2 B3 C1 C2 C3 D1 D2 D3 O); trivial. 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. destruct (col_dec A B D) as [HCol2|HNCol2]. apply (t22_16_2aux1 noah A B C D A1 A2 A3 B1 B2 B3 C1 C2 C3 D1 D2 D3 O); trivial. 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. assert (Hdiff : O <> A /\ O <> B /\ O <> C /\ O <> D). assert_cols; repeat split; intro; subst O; Col. spliter. destruct (ex_defect A B O) as [S1 [T1 [U1 HDef1]]]; auto. destruct (ex_defect B C O) as [S2 [T2 [U2 HDef2]]]; auto. destruct (ex_defect C D O) as [S3 [T3 [U3 HDef3]]]; auto. destruct (ex_defect A D O) as [S4 [T4 [U4 HDef4]]]; auto. destruct (t22_16_1bis noah A B C O S1 T1 U1 S2 T2 U2 D1 D2 D3) as [HIsi12 HSuma12]; trivial. apply defect_perm_132, HDef2. destruct (t22_16_1bis noah A D C O S4 T4 U4 S3 T3 U3 B1 B2 B3) as [HIsi34 HSuma34]; trivial. apply defect_perm_231, HDef3. destruct (t22_16_1bis noah B A D O S1 T1 U1 S4 T4 U4 C1 C2 C3) as [HIsi14 HSuma14]; trivial. apply defect_perm_213, HDef1. apply defect_perm_132, HDef4. apply defect_perm_213, HDefC. destruct (t22_16_1bis noah B C D O S2 T2 U2 S3 T3 U3 A1 A2 A3) as [HIsi23 HSuma23]; trivial. apply defect_perm_132, HDef3. apply defect_perm_213, HDefA. suma.assert_diffs. destruct (ex_suma D1 D2 D3 S3 T3 U3) as [V [W [X HSuma1]]]; auto. assert (HIsi1 : SAMS D1 D2 D3 S3 T3 U3). apply sams_lea2__sams with D1 D2 D3 B1 B2 B3; Lea; apply (sams_suma__lea456789 S4 T4 U4); trivial. assert (HSuma2 : SumA V W X S4 T4 U4 P Q R). apply suma_assoc_2 with D1 D2 D3 S3 T3 U3 B1 B2 B3; SumA. assert (HIsi2 : SAMS V W X S4 T4 U4). apply sams_assoc_2 with D1 D2 D3 S3 T3 U3 B1 B2 B3; SumA. assert (HSuma3 : SumA A1 A2 A3 S1 T1 U1 V W X). apply suma_assoc_2 with S3 T3 U3 S2 T2 U2 D1 D2 D3; SumA. assert (HIsi3 : SAMS A1 A2 A3 S1 T1 U1). apply sams_assoc_2 with S3 T3 U3 S2 T2 U2 D1 D2 D3; SumA. split. apply sams_assoc_2 with S4 T4 U4 S1 T1 U1 V W X; SumA. apply suma_assoc_2 with S4 T4 U4 S1 T1 U1 V W X; SumA. Qed.
imports: GeoCoq.Tarski_dev.Annexes.saccheri