proposition: Lemma bigA_distr_bigA (I J : finType) F : \big[*%M/1]_(i : I) \big[+%M/0]_(j : J) F i j = \big[+%M/0]_(f : {ffun I -> J}) \big[*%M/1]_i F i (f i).
proof: Proof. by rewrite bigA_distr_big; apply: eq_bigl => ?; apply/familyP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)