proposition: Lemma bigA_distr_big (I J : finType) (Q : pred J) (F : I -> J -> R) : \big[*%M/1]_i \big[+%M/0]_(j | Q j) F i j = \big[+%M/0]_(f in ffun_on Q) \big[*%M/1]_i F i (f i).
proof: Proof. exact: bigA_distr_big_dep. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)