proposition: Lemma tree_node_inv l k (t : tree l.+1 k) : exists (s : seq (tree l (negk k))), t = Node s.
proof: Proof. Proof match t with Node l' k' s => ex_intro _ _ erefl end. Lemma tree_node_children l k (t : tree l.+1 k) : t = Node (tree_children t). Proof. by case: (tree_node_inv t) => s ->. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist