proposition: Lemma perm_big_supp_cond [r s : seq I] [P : pred I] (F : I -> R) : perm_eq [seq i <- r | P i && (F i != idx)] [seq i <- s | P i && (F i != idx)] -> \big[op/idx]_(i <- r | P i) F i = \big[op/idx]_(i <- s | P i) F i.
proof: Proof. move=> prs; rewrite !(bigID [pred i | F i == idx] P F)/=. rewrite big1 ?Monoid.mul1m; last by move=> i /andP[_ /eqP->]. rewrite [in RHS]big1 ?Monoid.mul1m; last by move=> i /andP[_ /eqP->]. by rewrite -[in LHS]big_filter -[in RHS]big_filter; apply perm_big. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)