proposition: Lemma reindex : forall (I J : finType) (h : J -> I) (P : pred I) F, {on [pred i | P i], bijective h} -> \big[*%M/1]_(i | P i) F i === \big[*%M/1]_(j | P (h j)) F (h j).
proof: Proof. move=> I J h P F [h' hK h'K]; rewrite -> (reindex_onto _ h'K); apply eq_bigl=> j//=. by rewrite !inE; case Pi: (P _); rewrite //= hK ?eqxx. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops