fact: Definition fintree_dist l (t : @fintree tw l) := match ft t with | Node _ _ s => if (s != [::]) then tree_dist_children kv (size s).-1 (map (@tree_dist _ _) s) else 0 | Frontier _ => 1 end.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist