proposition: Lemma existential_saccheri__rah : postulate_of_existence_of_a_right_saccheri_quadrilateral -> postulate_of_right_saccheri_quadrilaterals.
proof: Proof. intro HABCD. destruct HABCD as [A [B [C [D [HSac HPer]]]]]. apply (per_sac__rah A B C D HSac HPer). Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Annexes.saccheri