proposition: Lemma aristotle__acute_or_right : aristotle_s_axiom -> hypothesis_of_acute_saccheri_quadrilaterals \/ hypothesis_of_right_saccheri_quadrilaterals.
proof: Proof. intros aristotle. destruct saccheri_s_three_hypotheses as [Ha|[Hr|Ho]]; auto. exfalso; apply aristotle__obtuse_case_elimination in aristotle; auto. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.saccheri