proposition: Lemma big_filter_cond : forall 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. move=> r P1 P2 F; rewrite <- big_filter, <- (big_filter r). apply congr_big=> [|i|]; try reflexivity. by rewrite -filter_predI; apply: eq_filter => i; exact: andbC. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops