proposition: Lemma nseqs_deg m (xs : seq (tree _ _)) : count_mem xs (nseqs en m) = ((size xs == m) && all (fun x => max_deg x <= n) xs)%nat.
proof: Proof. elim: m xs => [ [] // | m IH ] xs. case Hsz: (size _ == _). case: xs Hsz => //= x xs /eqP[xsm]. rewrite (@count_allpairs _ _ _ _ _ _ (pred1 x) (pred1 xs)) //. by rewrite en_full IH mulnb xsm eqxx andTb. apply/count_memPn. by apply: contraFN Hsz => /size_nseqs /eqP. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist