proposition: Lemma all_max_def_tree_enum l k : all (fun x => max_deg x <= n)%nat (tree_enum l k).
proof: Proof. apply/allP => x Hx. rewrite leqNgt; apply/negP => Hx'. move: (tree_enumP x). rewrite leqNgt // Hx' => /count_memPn. by rewrite Hx. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist