proposition: Lemma big_filter_cond r (P1 P2 : pred I) F : \big[op/idx]_(i <- filter P1 r | P2 i) F i = \big[op/idx]_(i <- r | P1 i && P2 i) F i.
proof: Proof. rewrite -big_filter -(big_filter r); congr bigop. by rewrite -filter_predI; apply: eq_filter => i; apply: andbC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)