proposition: Lemma INR_IPR : forall p, INR (Pos.to_nat p) = IPR p.
proof: Proof. induction p as [p IH | p IH |]. - now rewrite Pos2Nat.inj_xI, IPR_xI, S_INR, mult_INR, IH. - now rewrite Pos2Nat.inj_xO, mult_INR, IPR_xO, IH. - reflexivity. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField