proposition: Lemma lt_IPR : forall p q:positive, (p < q)%positive -> IPR p < IPR q.
proof: Proof. pose proof IPR_gt_0 as H; pose proof Rlt_0_2 as H'. induction p as [| p IH] using Pos.peano_ind; intros q Hq. - rewrite IPR_xH; induction q as [q IH' | [ q | q |] IH' |]. + rewrite IPR_xI, <-(Rplus_0_l 1) at 1. now apply Rplus_lt_compat_r, Rmult_lt_0_compat. + rewrite IPR_xO, <-(Rplus_0_l 1), <-Rplus_diag. apply Rplus_lt_compat; try easy; apply IH'; constructor. + rewrite IPR_xO, <-(Rplus_0_l 1), <-Rplus_diag. apply Rplus_lt_compat; try easy; apply IH'; constructor. + rewrite IPR_xO, IPR_xH. rewrite <-(Rplus_0_l 1) at 1; rewrite <-Rplus_diag. now apply Rplus_lt_compat_r, Rlt_0_1. + discriminate. - destruct q as [| q'] using Pos.peano_ind. + now exfalso; apply (Pos.nlt_1_r (Pos.succ p)). + now rewrite 2 succ_IPR; apply Rplus_lt_compat_l, IH, Pos.succ_lt_mono. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField