proposition: Lemma big_imset_cond h (A : {pred I}) (P : pred J) G : {in A &, injective h} -> \big[aop/idx]_(j in h @: A | P j) G j = \big[aop/idx]_(i in A | P (h i)) G (h i).
proof: Proof. by move=> h_inj; rewrite 2!big_mkcondr big_imset. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)