proposition: Lemma cancel_fintree n l : @cancel _ _ (@ft n l) (@fintree_decode n l).
proof: Proof. case=> t Ht. rewrite /fintree_decode. move: (limit_get_fintree n t). rewrite (limit_get_id Ht) => Ht'. congr mkFintree. by apply eq_irrelevance. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist