proposition: Lemma cancel_tree l k : cancel (@encode_tree l k) (@decode_tree l k).
proof: Proof. elim: l k => [|l IH] k t. - by rewrite (tree_frontier t). - rewrite (tree_node_children t) /=. f_equal. elim: (tree_children t) => [|t' ts' IH'] //=. by rewrite IH IH'. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist