proposition: Lemma size_finseqs n s : s \in finseqs n -> (size s <= n)%nat.
proof: Proof. case/flattenP => l /mapP [m]. by rewrite mem_iota leq0n add0n /= => mn -> /size_nseqs ->. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist