proposition: Lemma rectangle_existence__rah : postulate_of_existence_of_a_right_lambert_quadrilateral -> postulate_of_right_saccheri_quadrilaterals.
proof: Proof. intros HABCD. destruct HABCD as [A [B [C [D []]]]]. apply (lam_per__rah A B C D); assumption. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Annexes.saccheri