proposition: Lemma sumn_map_condE (T : Type) (s : seq T) (f : T -> nat) (P : pred T) : sumn [seq f i | i <- s & P i] = \sum_(i <- s | P i) f i.
proof: Proof. by rewrite /sumn foldrE big_map big_filter. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)