proposition: Lemma bigA_distr_big_dep (I J : finType) (Q : I -> pred J) F : \big[*%M/1]_i \big[+%M/0]_(j | Q i j) F i j = \big[+%M/0]_(f in family Q) \big[*%M/1]_i F i (f i).
proof: Proof. have [j _ | J0] := pickP J; first by rewrite (big_distr_big_dep j). have Q0 i: Q i =i pred0 by move=> /J0/esym/notF[]. transitivity (iter #|I| ( *%M 0) 1). by rewrite -big_const; apply/eq_bigr=> i; have /(big_pred0 _)-> := Q0 i. have [i _ | I0] := pickP I. rewrite (cardD1 i) //= mul0m big_pred0 // => f. by apply/familyP=> /(_ i); rewrite Q0. have f: I -> J by move=> /I0/esym/notF[]. rewrite eq_card0 // (big_pred1 (finfun f)) ?big_pred0 // => g. by apply/familyP/eqP=> _; first apply/ffunP; move=> /I0/esym/notF[]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)