fact: Fixpoint decode_tree l k (t : GenTree.tree unit) : tree l k := match l with | O => Frontier k | l'.+1 => match t with | GenTree.Leaf _ => Node [::] | GenTree.Node _ s => Node (map (@decode_tree l' (negk k)) s) end end.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist