proposition: 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: Proof. intros noah A B C C1 D E F G H I K L M HBet HDefA HDefC HSuma. assert (HDA := defect_distincts A B C1 D E F HDefA). assert (HDC := defect_distincts B C1 C G H I HDefC). spliter; clean. apply defect_perm_321 in HDefA. destruct HDefA as [P [Q [R [HTri HSuppa]]]]. assert (HSuma1 : SumA P Q R D E F A C1 C) by SumA. destruct HTri as [S [T [U [HSuma2 HSuma3]]]]. assert (HInter : SumA S T U D E F B C1 C /\ SAMS S T U D E F). { suma.assert_diffs. assert (HSuma4 : SumA B C1 C A C1 B A C1 C) by SumA. destruct (ex_suma A C1 B D E F) as [V [W [X HSuma5]]]; auto. assert (HIsi : SAMS P Q R D E F) by (apply suppa__sams; trivial). assert (HIsi1 : SAMS S T U A C1 B) by (apply (t22_20 noah), HSuma2). assert (HIsi2 : SAMS A C1 B D E F). { apply sams_lea2__sams with P Q R D E F; Lea. apply (sams_suma__lea456789 S T U); trivial. } 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). assert (HIsi3 : SAMS 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. split; trivial. destruct (ex_suma S T U D E F) as [B' [C1' [C' HSuma']]]; auto. 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). apply (conga3_suma__suma S T U D E F B' C1' C'); try (apply conga_refl); auto. apply (suppa2__conga456 A C1 B). apply suppa_sym, bet_suma__suppa with A C1 C; assumption. apply bet__suppa; auto. } clear dependent P; clear Q R. destruct HInter as [HSuma3 HIsi3]. apply defect_perm_231 in HDefC. destruct HDefC as [P [Q [R [HTri HSuppa]]]]. assert (HSuma1 : SumA P Q R G H I A C1 C) by SumA. destruct HTri as [V [W [X [HSuma4 HSuma5]]]]. assert (HIsi1 : SAMS P Q R G H I) by (apply bet_suma__sams with A C1 C; trivial). assert (HIsi5 : SAMS V W X B C1 C) by (apply (t22_20 noah), HSuma4). assert (HIsi : SAMS D E F G H I). { apply sams_lea2__sams with P Q R G H I; Lea. apply lea_trans with B C1 C. apply (sams_suma__lea456789 S T U); trivial. apply (sams_suma__lea456789 V W X); trivial. } split; trivial. suma.assert_diffs. destruct (ex_suma V W X S T U) as [A' [B' [C' HSuma6]]]; auto. assert (HIsi6 : SAMS V W X S T U). { apply sams_lea2__sams with V W X B C1 C; Lea. apply sams_suma__lea123789 with D E F; trivial. } 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). assert (HSuma8 : SumA A' B' C' K L M A C1 C). { apply suma_assoc_1 with D E F G H I P Q R; trivial. apply sams_assoc_2 with V W X S T U B C1 C; trivial. } exists A', B', C'. 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. destruct (ex_suma V W X C1 B A) as [D [E [F HSuma]]]; auto. assert (HIsi : SAMS V W X C1 B A). { apply sams_lea2__sams with V W X S T U; Lea. apply sams_suma__lea123789 with B A C1; SumA. } suma.assert_diffs. apply trisuma_perm_132. exists D, E, F. split. - assert (HConga : CongA C1 C B A C B). apply out2__conga; [apply l6_6, bet_out|apply out_trivial]; Between. apply (conga3_suma__suma C1 C B C B A D E F); CongA. assert (HInAngle : InAngle C1 C B A). repeat split; auto; exists C1; split; Between; right; apply out_trivial; auto. apply suma_assoc_1 with C B C1 C1 B A V W X; SumA. - assert (HConga : CongA B A C B A C1). apply out2__conga; [apply out_trivial|apply bet_out]; auto. apply (conga3_suma__suma D E F B A C1 A' B' C'); CongA. apply suma_assoc_2 with V W X C1 B A S T U; SumA. Qed.
imports: GeoCoq.Tarski_dev.Annexes.saccheri