Library GeoCoq.Meta_theory.Parallel_postulates.rah_rectangle_principle

Require Import GeoCoq.Axioms.parallel_postulates.
Require Import GeoCoq.Tarski_dev.Annexes.saccheri.

Section rah_rectangle_principle.

Context `{T2D:Tarski_2D}.

Lemma rah__rectangle_principle : postulate_of_right_saccheri_quadrilaterals → postulate_of_right_lambert_quadrilaterals.
Proof.
intros rah A B C D HLam.
apply (lam_per__rah A); assumption.
Qed.

End rah_rectangle_principle.