proposition: Lemma thales_existence__rah : existential_thales_postulate -> postulate_of_right_saccheri_quadrilaterals.
proof: Proof. intro thales. destruct thales as [A [B [C [M]]]]. spliter. apply (t22_17__rah A B C M); assumption. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Annexes.saccheri