proposition: Lemma coef_deriv p i : nth (deriv tt p) i = (nth p i.+1 * INR i.+1)%R.
proof: Proof. rewrite /deriv /deriv_loop -{2}[in RHS]addn1. elim: p i 1 => [|a p IHp] i n; first by rewrite /nth !nth_nil Rmult_0_l. case: p IHp => [|b p] IHp; first by rewrite /= /nth !nth_nil Rmult_0_l. case: i => [|i] //=. rewrite IHp; congr Rmult. by rewrite addnS. Qed.
imports: Coq(ZArith Reals) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Flocq(Core) Stdlib MathComp Interval Xreal Basic_rec