proposition: Lemma f1 l : \sum_(t : @fintree tw l) (@fintree_dist l t) = 1.
proof: Proof. rewrite /index_enum /=. have ->: Finite.enum (fintree_finType tw l) = fintree_enum tw l. by rewrite unlock /=. rewrite /fintree_enum. destruct (fintree_enum_dep _ _) => /=. rewrite /fintree_dist. transitivity (\sum_(t<-map (@ft _ _) x) match t with | Frontier _ => 1 | Node l k [::] => 0 | Node l k ((_ :: _) as s) => tree_dist_children kv (size s).-1 [seq tree_dist i | i <- s] end). symmetry. rewrite big_map. apply eq_bigr => i _. case (ft i) => // l0 k s. by case s. rewrite {}e {x}. case: l => [|l]. by rewrite /= big_seq1. rewrite doubleS -addn1 /=. rewrite big_cons add0r big_map big_flatten. rewrite big_map /=. rewrite (iotaDl 1 0) big_map. rewrite /tree_dist_children. transitivity (\sum_(0 <= d < tw) (LR kv)`_d); last first. have: (size (LR kv) <= tw)%nat. by rewrite /LR /norm_integ_deg size_norm size_integ. destruct (LR kv) => /= Hsz. rewrite (@horner_coef_wide _ tw) // in p1. rewrite -p1. rewrite big_mkord. apply eq_bigr => i _. by rewrite expr1n mulr1. rewrite /index_iota subn0. apply eq_bigr => d _. rewrite -/(addn l.*2 1). transitivity (\sum_(s <- nseqs (tree_enum tw (l.*2+1) kf) (1+d)) (LR kv)`_d * \prod_(t <- s) tree_dist t). rewrite big_seq [in X in _ = X]big_seq. apply eq_bigr => s /size_nseqs. case: s => [|a s] // [] Hs. by rewrite big_map /= Hs. move: (1+d)%nat => d'. rewrite -big_distrr /=. rewrite -[X in _ = X]mulr1. f_equal. elim: d' => [|d1 IHd] /=. by rewrite big_seq1 big_nil. rewrite (@allpairs_flatten _ _ _ (fun s t => s :: t)) big_flatten big_map /=. rewrite -[X in _ = X](f1_tree (l.*2+1) kf). apply eq_bigr=> t1 _. rewrite big_map /=. rewrite -[X in _ = X]mulr1 -[in X in _ = X]IHd. rewrite big_distrr /=. apply eq_bigr=> tl _. by rewrite big_cons. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist