proposition: Lemma tree_frontier k (t : tree O k) : t = Frontier k.
proof: Proof. Proof match t with Frontier _ => erefl end. Lemma tree_children_node l k (s : seq (tree l (negk k))) : tree_children (Node s) = s. Proof. by []. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist