proposition: Lemma mcoeff_deriv i m p : p^`M(i)@_m = p@_(m + U_(i)) *+ (m i).+1.
proof: Proof. pose_big_enough j; first rewrite {2}[p](mpolywE (k := j)) //. rewrite !(mderivwE j) // !raddf_sum -sumrMnl; apply/eq_bigr. move=> /= [k /= _] _; rewrite !mcoeffZ !mcoeffX. case: (k =P m + U_(i))%MM=> [{1 3}->|]. by rewrite mnmDE mnm1E eqxx addn1 addmK eqxx !simpm mulr_natl. rewrite !simpm mul0rn; have [->|nz_mi] := (eqVneq (k i) 0%N). by rewrite !simpm. case: eqP=> [{1}<-|]; rewrite ?simpm //. rewrite submK //; apply/mnm_lepP => l; rewrite mnm1E. by case: (i =P l) nz_mi=> // ->; rewrite -lt0n. by close. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg