proposition: Lemma big_imset_idem [I J : finType] (h : I -> J) (A : pred I) F : idempotent op -> \big[op/x]_(j in h @: A) F j = \big[op/x]_(i in A) F (h i).
proof: Proof. rewrite -!big_image => op_idem; rewrite -big_undup// -[RHS]big_undup//. apply/perm_big/perm_undup => j; apply/imageP. have [mem_j | /imageP mem_j] := boolP (j \in [seq h j | j in A]). - by exists j => //; apply/imsetP; apply: imageP mem_j. - by case=> k /imsetP [i j_in_A ->] eq_i; apply: mem_j; exists i. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)