proposition: Lemma reindex (I J : finType) (h : J -> I) (P : pred I) F : {on [pred i | P i], bijective h} -> \big[op/x]_(i | P i) F i = \big[op/x]_(j | P (h j)) F (h j).
proof: Proof. case=> h' hK h'K; rewrite (reindex_onto h h' h'K). by apply: eq_bigl => j /[!inE]; case Pi: (P _); rewrite //= hK ?eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)