proposition: Lemma eq_big_perm : forall (I : eqType) r1 r2 (P : pred I) F, 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=> I r1 r2 P F; move/perm_eqP; rewrite -> !(big_mkcond _ P). elim: r1 r2 => [|i r1 IHr1] r2 eq_r12. by case: r2 eq_r12 => //;try reflexivity; move=> 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 -> left_commut; apply op_morph; [reflexivity|]; rewrite <- big_cat; apply: IHr1 => a. move/(_ a): eq_r12; rewrite !count_cat /= addnCA; exact: addnI. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops