proposition: Lemma archi__obtuse_case_elimination : archimedes_axiom -> ~ hypothesis_of_obtuse_saccheri_quadrilaterals.
proof: Proof. intros archi obtuse. destruct ex_saccheri as [A [B [C [D HSac]]]]. absurd(Obtuse A B C). apply t22_19 with D; trivial. apply obtuse with D; trivial. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.saccheri GeoCoq.Tarski_dev.Ch13_1 GeoCoq.Meta_theory.Continuity.grad