proposition: Lemma big_distr_big (I J : finType) j0 (P : pred I) (Q : pred J) F : \big[*%M/1]_(i | P i) \big[+%M/0]_(j | Q j) F i j = \big[+%M/0]_(f in pffun_on j0 P Q) \big[*%M/1]_(i | P i) F i (f i).
proof: Proof. rewrite (big_distr_big_dep j0); apply: eq_bigl => f. by apply/familyP/familyP=> Pf i; case: ifP (Pf i). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)