fact: Record fintree (n l : nat) : Type := mkFintree { ft :> tree l.*2 kv ; _ : (max_deg ft <= n)%nat }.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist