proposition: Lemma fintree_enumP n l : Finite.axiom (@fintree_enum n l).
proof: Proof. rewrite /fintree_enum. destruct fintree_enum_dep as [s Hs] => /= t. have Hun: uniq s. move/(congr1 uniq) : Hs. by rewrite uniq_tree_enum => /map_uniq. rewrite count_uniq_mem //. have /mapP [x Hx1 Hx2] : ft t \in [seq ft i | i <- s]. move: (@count_uniq_mem _ [seq ft i | i <- s] t). rewrite Hs uniq_tree_enum tree_enumP => /(_ erefl). destruct t. rewrite i. by case: (_ \in _). by rewrite (can_inj (@cancel_fintree n l) Hx2) Hx1. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist