proposition: Lemma reindex_onto (I J : finType) (h : J -> I) h' (P : pred I) (F : I -> X) : (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=> h'K; elim: {P}_.+1 {-3}P h'K (ltnSn #|P|) => //= n IHn P h'K. case: (pickP P) => [i Pi | P0 _]; last first. by rewrite !big_pred0 // => j; rewrite P0. rewrite ltnS (cardD1x Pi); move/IHn {n IHn} => IH. rewrite (bigD1 i Pi) (bigD1 (h' i)) h'K ?Pi ?eq_refl //=. apply: mon_eqv => //. rewrite {}IH => [|j]; [apply: eqv_bigl => j | by case/andP; auto]. rewrite andbC -andbA (andbCA (P _)); case: eqP => //= hK; congr (_ && ~~ _). by apply/eqP/eqP=> [<-|->] //; rewrite h'K. Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect)