fact: Fixpoint nseqs (n : nat) : seq (seq A) := match n with | O => [:: [::]] | n'.+1 => allpairs (Cons A) en (nseqs n') end.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist