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