proposition: Lemma eq_bigl : forall r (P1 P2 : pred I) F, P1 =1 P2 -> \big[op/idx]_(i <- r | P1 i) F i === \big[op/idx]_(i <- r | P2 i) F i.
proof: Proof. move=> r P1 P2 F eqP12; rewrite <- big_filter, (eq_filter eqP12), big_filter; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops