proposition: Lemma IPR_le : forall p q:positive, IPR p <= IPR q -> (p <= q)%positive.
proof: Proof. intros p q [I | E]. - now apply Pos.lt_le_incl, IPR_lt. - now apply IPR_eq in E as ->; apply Pos.le_refl. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField