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