proposition: Lemma rah__rectangle_principle : postulate_of_right_saccheri_quadrilaterals -> postulate_of_right_lambert_quadrilaterals.
proof: Proof. intros rah A B C D HLam. apply (lam_per__rah A); assumption. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Annexes.saccheri