proposition: Lemma partition_big_imset h (A : {pred I}) F : \big[aop/idx]_(i in A) F i = \big[aop/idx]_(j in h @: A) \big[aop/idx]_(i in A | h i == j) F i.
proof: Proof. by apply: partition_big => i Ai; apply/imsetP; exists i. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)