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