proposition: Lemma reindex_onto : forall (I J : finType) (h : J -> I) h' (P : pred I) F, (forall i, P i -> h (h' i) = i) -> \big[*%M/1]_(i | P i) F i === \big[*%M/1]_(j | P (h j) && (h' (h j) == j)) F (h j).
proof: Proof. move=> I J h h' P F h'K. elim: {P}_.+1 {-3}P h'K (ltnSn #|P|) => //= n IHn P h'K. case: (pickP P) => [i Pi | P0 _]; last first. rewrite -> big_pred0=> //; rewrite -> big_pred0=> //; [reflexivity|]. by move=> j //=; rewrite P0. rewrite ltnS (cardD1x Pi); move/IHn {n IHn} => IH. rewrite -> (bigD1 (j:=i) _ Pi), (bigD1 (j:=h' i)); rewrite h'K ?Pi ?eq_refl //=; apply op_morph; try reflexivity. rewrite -> IH. apply eq_bigl=> j//=; rewrite andbC -andbA (andbCA (P _)). by case: eqP => //= hK; congr (_ && ~~ _); apply/eqP/eqP=> [<-|->] //; rewrite h'K. by move=> j//=; case/andP; auto. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops