proposition: Lemma Node_inj l k : injective (@Node l k).
proof: Proof. move=> s s' H. by rewrite (_ : s = tree_children (Node s)) // H. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist