proposition: Lemma big_imset h (A : {pred I}) G : {in A &, injective h} -> \big[aop/idx]_(j in h @: A) G j = \big[aop/idx]_(i in A) G (h i).
proof: Proof. move=> injh; pose hA := mem (image h A). rewrite (eq_bigl hA) => [|j]; last exact/imsetP/imageP. pose h' := omap (fun u : {j | hA j} => iinv (svalP u)) \o insub. rewrite (reindex_omap h h') => [|j hAj]; rewrite {}/h'/= ?insubT/= ?f_iinv//. apply: eq_bigl => i; case: insubP => [u /= -> def_u | nhAhi]; last first. by apply/andP/idP => [[]//| Ai]; case/imageP: nhAhi; exists i. set i' := iinv _; have Ai' : i' \in A := mem_iinv (svalP u). by apply/eqP/idP => [[<-] // | Ai]; congr Some; apply: injh; rewrite ?f_iinv. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)