fact: Fixpoint max_deg (l : nat) k (t : tree l k) : nat := match t with | Frontier _ => O | Node l' k' s => foldr maxn (size s) (map (@max_deg _ _) s) end.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist