proposition: Lemma IPR_eq : forall p q:positive, IPR p = IPR q -> p = q.
proof: Proof. intros p q HR. destruct (Pos.eq_dec p q) as [E | NE]; [assumption |]. now apply not_IPR in NE. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField