proposition: Lemma t22_19 : archimedes_axiom -> forall A B C D, Saccheri A B C D -> ~ Obtuse A B C.
proof: Proof. intros archi A B C D HSac HObt. assert (H := t22_18 archi _ _ _ _ (sac_perm _ _ _ _ HSac)). apply H. apply lt_left_comm; apply <- lt_sac__obtuse; auto. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.saccheri GeoCoq.Tarski_dev.Ch13_1 GeoCoq.Meta_theory.Continuity.grad