proposition: Lemma tree_enumP l k (x : tree l k) : count_mem x (tree_enum l k) = (max_deg x <= n)%nat.
proof: Proof. elim: l k x => [|l IH] k x. by rewrite (tree_frontier x) /= addn0. rewrite (tree_node_children x). rewrite -(@finseqs_deg n l k (tree_enum l (negk k))); last by []. rewrite {IH} /=. congr addn. - rewrite eqtype.inj_eq //. by apply Node_inj. - rewrite count_map. apply eq_count => s /=. rewrite eqtype.inj_eq //. by apply Node_inj. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist