proposition: Lemma limit_get_fintree l k (t : tree l k) : (max_deg (limit_get t) <= n)%nat.
proof: Proof. elim: l k t => [|l IH] k t. - by rewrite (tree_frontier t). - rewrite (tree_node_children t) /= foldr_maxnE. apply/andP; split. + by rewrite size_take_leq. + apply/allP => m /mapP [t0 /mem_take/mapP [t2 Ht2 ->{t0} ->{m}]]. by apply IH. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist