proposition: Lemma not_IPR : forall p q:positive, p <> q -> IPR p <> IPR q.
proof: Proof. intros p q. destruct (Pos.lt_total p q) as [Hlt | [Eq | Hgt]]; intros H. - now apply Rlt_not_eq, lt_IPR. - easy. - now apply not_eq_sym, Rlt_not_eq, lt_IPR. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField