proposition: Lemma split_sumZ_fs (P : Z -> R) (C : pred {ffun 'I_k -> 'I_l}): \sum_(fz : Z | C fz.1) (P fz) = \sum_(f: {ffun 'I_k -> 'I_l} | C f) (\sum_(s: 'S_k) (P (f,s))).
proof: Proof. rewrite pair_big /=. by apply/eq_big; case=>//= [f s]; rewrite andbT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor