proposition: Lemma perm_big (I : eqType) r1 r2 (P : pred I) (F : I -> X) : perm_eq r1 r2 -> \big[*%M/1]_(i <- r1 | P i) F i ≡ \big[*%M/1]_(i <- r2 | P i) F i.
proof: Proof. move/permP; rewrite !(big_mkcond _ P). elim: r1 r2 => [|i r1 IHr1] r2 eq_r12. by case: r2 eq_r12 => // i r2; move/(_ (pred1 i)); rewrite /= eqxx. have r2i: i \in r2 by rewrite -has_pred1 has_count -eq_r12 /= eqxx. case/splitPr: r2 / r2i => [r3 r4] in eq_r12 *. rewrite big_cat /= !big_cons. rewrite monA [_ ⊗ if _ then _ else _]monC -monA. rewrite -big_cat. rewrite (IHr1 (r3 ++ r4)) //. move => a. move/(_ a) : eq_r12. rewrite !count_cat /= addnCA. apply: addnI. Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect)