proposition: Lemma finseqs_deg (xs : seq (tree l (negk k))) : (count_mem xs (finseqs en n) = (max_deg (Node xs) <= n))%nat.
proof: Proof. rewrite max_deg_all. elim: {1 2}n => [ | m IH ]. by case: xs. rewrite /finseqs /mkseq -addn1 iotaD map_cat flatten_cat count_cat. rewrite [in X in (_ + X)%nat = _]/= cats0 IH. case: leqP => Hm. rewrite ltnW //= (_ : count_mem _ _ = O) // ?addn0 //. suff /count_memPn -> : xs \notin nseqs en m.+1 by []. apply: contraL Hm => /size_nseqs ->. by rewrite ltnn. by rewrite /= add0n leq_eqVlt ltnS leqNgt Hm orbF (nseqs_deg m.+1 xs). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist