proposition: Lemma mcoeff_mderiv i p m : (p^`M(i))@_m = p@_(m + U_(i)) *+ (m i).+1.
proof: Proof. rewrite -mderivmU1m mcoeff_mderivm addmC /=. rewrite (bigD1 i) //= mnmDE !mnm1E eqxx addn1 ffactn1. rewrite (eq_bigr (fun _ => 1%N)) ?prod_nat_const /=. by rewrite exp1n muln1. move=> j ne_ji; rewrite mnmDE mnm1E eq_sym. by rewrite (negbTE ne_ji) ffactn0. 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