proposition: Lemma mcoeff_mderivm m p m' : (p^`M[m])@_m' = p@_(m + m') *+ (\prod_(i < n) ((m + m')%MM i)^_(m i)).
proof: Proof. pose_big_enough i; first rewrite (@mderivmwE i) //. have lt_mDm'_i: mdeg (m + m') < i by []. rewrite (bigD1 (Sub (m + m')%MM lt_mDm'_i)) //=. rewrite mcoeffD raddf_sum /= [X in _+X]big1; last first. case=> j lt_ji; rewrite eqE /= => ne_j_mDm'. rewrite mcoeffZ mcoeffX; case: eqP; rewrite ?mulr0 //=. move=> eq_m'_jBm; move: ne_j_mDm'; rewrite -eq_m'_jBm. case: (boolP (m <= j))%MM => [/addmBA->|]. by rewrite [(m + j)%MM]addmC /= addmK eqxx. rewrite negb_forall; case/existsP=> /= k Nle_mj. by rewrite (bigD1 k) //= ffact_small ?simpm // ltnNge. rewrite addr0 mcoeffZ mcoeffX {3}[(m + m')%MM]addmC addmK. by rewrite eqxx mulr1 mulr_natr. 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