proposition: Lemma size_deriv (p : {poly R}) : size p^`() = (size p).-1.
proof: Proof. have [lep1|lt1p] := leqP (size p) 1. by rewrite {1}[p]size1_polyC // derivC size_poly0 -subn1 (eqnP lep1). rewrite size_poly_eq // mulrn_eq0 -subn2 -subSn // subn2. by rewrite lead_coef_eq0 -size_poly_eq0 -(subnKC lt1p). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(ssralg poly ssrnum zmodp polydiv interval)