proposition: Lemma reindex_omap (I J : finType) (h : J -> I) h' (P : pred I) F : (forall i, P i -> omap h (h' i) = some i) -> \big[op/x]_(i | P i) F i = \big[op/x]_(j | P (h j) && (h' (h j) == some j)) F (h j).
proof: Proof. move=> h'K; have [n lePn] := ubnP #|P|; elim: n => // n IHn in P h'K lePn *. case: (pickP P) => [i Pi | P0]; last first. by rewrite !big_pred0 // => j; rewrite P0. have := h'K i Pi; case h'i_eq : (h' i) => [/= j|//] [hj_eq]. rewrite (bigD1 i Pi) (bigD1 j) hj_eq ?Pi ?h'i_eq ?eqxx //=; congr (op : _ -> _). rewrite {}IHn => [|k /andP[]|]; [|by auto | by rewrite (cardD1x i) in lePn]. apply: eq_bigl => k; rewrite andbC -andbA (andbCA (P _)); case: eqP => //= hK. congr (_ && ~~ _); apply/eqP/eqP => [|->//]. by move=> /(congr1 h'); rewrite h'i_eq hK => -[]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)