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