proposition: Lemma mderivM i p q : (p * q)^`M(i) = (p^`M(i) * q) + (p * q^`M(i)).
proof: Proof. elim/mpolyind: p; first by rewrite !(mul0r, add0r, mderiv0). move=> c m p _ _ ih; rewrite !(mulrDl, mderivD) -addrA. rewrite [X in _=_+X]addrCA -ih addrA => {ih}; congr (_ + _). rewrite -!scalerAl !mderivZ -scalerAl -scalerDr; congr (_ *: _). pose_big_enough k; rewrite 1?[q](mpolywE (k := k)) //; try by close. do! rewrite mulr_sumr ?raddf_sum /=; rewrite -big_split /=. apply/eq_bigr=> h _; rewrite -!commr_mpolyX -scalerAl -mpolyXD. rewrite !mderivZ -commr_mderivX -!scalerAl -scalerDr; congr (_ *: _). rewrite !mderivX -!commr_mpolyX -!scalerAl -!mpolyXD mnmDE. have [z_mi|ne_mi] := eqVneq (m i) 0%N. rewrite z_mi addn0 scale0r add0r; congr (_ *: 'X_[_]). apply/mnmP=> j; rewrite !(mnmBE, mnmDE, mnm1E). by case: eqP => /= [<-|]; rewrite ?subn0 // z_mi !addn0. apply/esym; rewrite addmC addmBA; last by rewrite lep1mP. have [z_hi|ne_hi] := eqVneq (h i) 0%N. by rewrite z_hi add0n scale0r addr0. rewrite addrC addmC addmBA; last by rewrite lep1mP. by rewrite addmC -scalerDl natrD. 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