proposition: 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: Proof. intros A B C D E F oah HNCol HSuma1 HacuteB HacuteC HIsi. destruct (t22_14_aux A B C) as [A']; [assumption..|spliter]. assert_diffs. assert(HSuma2 := ex_suma D E F B C A). destruct HSuma2 as [P [Q [R HSuma2]]]; suma.assert_diffs; auto. absurd (LtA B A' C P Q R). apply (lea__nlta); apply l11_31_2; auto. assert(HSuma3 := ex_suma B A' A C A A'). rename H into HBet. destruct HSuma3 as [G [H [I HSuma3]]]; auto. assert(LtA G H I D E F). { assert(HSuma4 := ex_suma A' A B A B C). destruct HSuma4 as [V [W [X HSuma4]]]; auto. suma.assert_diffs. assert(SAMS C A A' A' A B). { apply os_ts__sams; Side. apply out_one_side; [Col|Out]. } assert(SAMS A' A B A B C) by (apply (conga2_sams__sams A' A B A B A'); SumA; CongA). assert(SumA C A A' A' A B C A B) by (exists B; repeat (split; CongA); Side; Cop). apply (sams_lea_lta456_suma2__lta C A A' B A' A _ _ _ C A A' V W X); Lea. 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. apply (sams_assoc _ _ _ A' A B A B C C A B); SumA. SumA. apply (suma_assoc _ _ _ A' A B A B C _ _ _ C A B); auto. } assert(HSuma4 := ex_suma C A A' B C A). destruct HSuma4 as [J [K [L HSuma4]]]; auto. suma.assert_diffs. assert(LtA A A' C J K L). 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. assert(HSuma5 := ex_suma B A' A J K L). destruct HSuma5 as [S [T [U HSuma5]]]; auto. suma.assert_diffs. 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]. apply (sams_assoc _ _ _ C A A' B C A G H I); auto. apply (conga2_sams__sams C A' A C A A'); SumA; CongA. apply (conga2_sams__sams C A A' A' C A); SumA; CongA. 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. apply (suma_assoc B A' A C A A' _ _ _ _ _ _ _ _ _ J K L); auto. apply (conga2_sams__sams C A' A C A A'); SumA; CongA. apply (conga2_sams__sams C A A' A' C A); SumA; CongA. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma