proposition: Lemma INR_IZR_INZ : forall n:nat, INR n = IZR (Z.of_nat n).
proof: Proof. intros [| n]. - reflexivity. - simpl Z.of_nat; unfold IZR; simpl IZR. now rewrite <-INR_IPR, SuccNat2Pos.id_succ. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField