proposition: Lemma R_from_nat_correct : forall p (b : I.type) (n : nat), contains (I.convert (I.fromZ p (Z.of_nat n))) (Xreal (INR n)).
proof: Proof. move=> p b n; rewrite INR_IZR_INZ; exact: I.fromZ_correct. Qed.
imports: Coq(ZArith Reals Psatz) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat bigop) Coquelicot(Coquelicot) Stdlib MathComp Xreal Interval Taylor