proposition: Lemma sumn_map_filter I s (f : I -> nat) P : sumn [seq f i | i <- s & P i] = \sum_(i <- s | P i) f i.
proof: Proof. by rewrite sumn_map big_filter. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap