proposition: Lemma IPR_lt : forall p q:positive, IPR p < IPR q -> (p < q)%positive.
proof: Proof. intros p q. generalize dependent p. induction q as [| q IH] using Pos.peano_ind; intros p H. - rewrite IPR_xH in H; exfalso; apply (Rle_not_lt (IPR p) 1); try easy. now apply IPR_ge_1. - destruct p as [| p] using Pos.peano_ind. + exact (Pos.lt_1_succ q). + apply ->Pos.succ_lt_mono; apply IH. rewrite 2!succ_IPR in H. now apply Rplus_lt_reg_l with (1 := H). Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField