proposition: Lemma perm_big_supp [r s : seq I] [P : pred I] (F : I -> R) : perm_eq [seq i <- r | F i != idx] [seq i <- s | F i != idx] -> \big[op/idx]_(i <- r | P i) F i = \big[op/idx]_(i <- s | P i) F i.
proof: Proof. by move=> ?; apply: perm_big_supp_cond; rewrite !filter_predI perm_filter. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)