fact: Hypothesis Poly_nth : forall (x : R) n k, dom x -> k <= n -> PolR.nth (P x n) k = Rdiv (Dn k x) (INR (fact k)).
imports: Coq(ZArith Psatz Reals) Flocq(Raux) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp Coquelicot Xreal Interval Basic Xreal_derive Interval_compl Datatypes Taylor_poly Basic_rec Bound