proposition: Lemma mderivmU1m i p : p^`M[U_(i)] = p^`M(i).
proof: Proof. rewrite mderivm_foldr (@mderiv_perm _ [:: i]) //. apply/seq.permP=> /= a; rewrite addn0 count_flatten sumnE !big_map. rewrite -/(index_enum _) (bigD1 i) //=. rewrite mnm1E eqxx /= big1 ?addn0 // => j ne_ji. by rewrite mnm1E eq_sym (negbTE ne_ji). 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