proposition: Lemma le_IPR : forall p q:positive, (p <= q)%positive -> IPR p <= IPR q.
proof: Proof. intros p q [I | ->]%Pos.le_lteq. - now left; apply lt_IPR. - now right. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField