proposition: Lemma not_1_IPR : forall p:positive, p <> 1%positive -> IPR p <> 1.
proof: Proof. intros p H; destruct p as [| p] using Pos.peano_ind. - now exfalso; apply H. - rewrite succ_IPR; apply Rgt_not_eq. rewrite <-(Rplus_0_r 1), IPR_xH. now apply Rplus_gt_compat_l, IPR_gt_0. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField