proposition: Lemma perm_big (I : eqType) r1 r2 (P : pred I) F : perm_eq r1 r2 -> \big[op/x]_(i <- r1 | P i) F i = \big[op/x]_(i <- r2 | P i) F i.
proof: Proof. elim: r1 r2 => [|i r1 IHr1] r2 eq_r12. by case: r2 eq_r12 => [//|i r2] /[1!perm_sym] /perm_nilP. have r2i: i \in r2 by rewrite -has_pred1 has_count -(permP eq_r12) /= eqxx. rewrite big_cons (IHr1 (rem i r2)) -?big_rem_AC// -(perm_cons i). exact: perm_trans (perm_to_rem _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)