proposition: Lemma mderiv_summ (T : Type) (r : seq T) (P : pred T) F p : p^`M[\sum_(x <- r | P x) (F x)] = foldr mderivm p [seq F x | x <- r & P x].
proof: Proof. elim: r => //= [|x s ih]; first by rewrite big_nil mderivm0m. by rewrite big_cons; case: (P x); rewrite //= addmC mderivmDm ih. 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