proposition: Lemma absolute_exterior_angle_theorem : ~ hypothesis_of_obtuse_saccheri_quadrilaterals -> forall A B C D E F B', Bet B A B' -> A <> B' -> SumA A B C B C A D E F -> LeA D E F C A B'.
proof: Proof. intros noah A B C D E F B' HBet HAB' HSuma. assert (HIsi := t22_20 noah A B C D E F HSuma). assert_diffs. apply sams_chara with B; SumA. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma