proposition: Lemma allpairs_flatten {S T R} (f : S -> T -> R) s t : [seq f i j | i <- s, j <- t] = flatten [seq [seq f x y | y <- t] | x <- s].
proof: Proof. elim: s => [|a s IH] //=; by f_equal. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist