proposition: Lemma mderiv_comm i j p : p^`M(i)^`M(j) = p^`M(j)^`M(i).
proof: Proof. pose_big_enough k; first pose mderivE := (mderivwE k). rewrite ![p^`M(_)]mderivE // !raddf_sum /=; apply/eq_bigr. move=> l _; rewrite !mderivZ !mderivX !scalerA. rewrite !submDA addmC -!commr_nat -!mulrA -!natrM. f_equal; congr (_ * _%:R); rewrite !mnmBE !mnm1E. by case: eqVneq => [->|_] //=; rewrite !subn0 mulnC. 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