proposition: Lemma derivn_poly0 : forall (p : {poly R}) n, (size p <= n)%N = (p^`(n) == 0).
proof: Proof. move=> p n; apply/idP/idP. move=> Hpn; apply/eqP; apply/polyP=>i; rewrite coef_derivn. rewrite nth_default; first by rewrite mul0rn coef0. by apply: leq_trans Hpn _; apply leq_addr. elim: n {-2}n p (leqnn n) => [m | n ihn [| m]] p. - by rewrite leqn0; move/eqP->; rewrite derivn0 leqn0 -size_poly_eq0. - by move=> _; apply: ihn; rewrite leq0n. - rewrite derivSn => hmn hder; case e: (size p) => [|sp] //. rewrite -(prednK (ltn0Sn sp)) [(_.-1)%N]lock -e -lock -size_deriv ltnS. exact: ihn. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(ssralg poly ssrnum zmodp polydiv interval)