proposition: Lemma eq_big_idem (I : eqType) (r1 r2 : seq I) (P : pred I) F : idempotent *%M -> r1 =i r2 -> \big[*%M/1]_(i <- r1 | P i) F i = \big[*%M/1]_(i <- r2 | P i) F i.
proof: Proof. move=> idM eq_r; rewrite -big_undup // -(big_undup r2) //; apply/perm_big. by rewrite uniq_perm ?undup_uniq // => i; rewrite !mem_undup eq_r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)