proposition: Lemma uniq_tree_enum l k : uniq (tree_enum l k).
proof: Proof. apply count_mem_uniq => t. case/boolP : (t \in _). rewrite -has_pred1 has_count tree_enumP. by case: (max_deg _ <= _)%nat. by apply/count_memPn. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist