proposition: Lemma eq_bigl 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. by move=> eqP12; rewrite -!(big_filter r) (eq_filter eqP12). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)