proposition: Lemma IPR_ge_1 : forall p:positive, 1 <= IPR p.
proof: Proof. pose proof (Rlt_0_1) as H; pose proof (Rlt_0_2) as H'. induction p as [p IH | p IH |]. - rewrite IPR_xI, <-(Rplus_0_l 1) at 1; apply Rplus_le_compat_r. apply Rmult_le_pos; try now left. now apply (Rle_trans _ 1); try apply IH; left. - rewrite IPR_xO, <-Rplus_diag, <-(Rplus_0_l 1); apply Rplus_le_compat; try easy. now apply (Rle_trans _ 1); try apply IH; left. - now rewrite IPR_xH; apply Rle_refl. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField