proposition: Lemma f1_tree l k : \sum_(t <- tree_enum tw l k) tree_dist t = 1.
proof: Proof. elim: l k => [|l IH] k. by rewrite /= big_seq1. rewrite big_map. transitivity (\sum_(ss <- mkseq (nseqs (tree_enum tw l (negk k))) tw.+1) \sum_(s <- ss) tree_dist (Node s)). by rewrite -big_flatten. rewrite big_map. set tw' := tw.+1. transitivity (\sum_(d < tw') (LR k)`_d); last first. have: (size (LR k) < tw')%nat. by destruct k; rewrite /LR /norm_integ_deg size_norm size_integ. destruct (LR k) => /= Hsz. rewrite (@horner_coef_wide _ tw') // in p1. rewrite -p1. apply eq_bigr => i _. by rewrite expr1n mulr1. by apply ltnW. rewrite (@big_mkord _ _ _ tw'). apply eq_bigr => d _. transitivity (\sum_(s <- nseqs (tree_enum tw l (negk k)) d) (LR k)`_d * \prod_(t <- s) tree_dist t). rewrite big_seq [in X in _ = X]big_seq. apply eq_bigr => s /size_nseqs /= ->. by rewrite /tree_dist_children big_map. rewrite -big_distrr /=. rewrite -[X in _ = X]mulr1. f_equal. elim: (val d) => [|d' IHd] /=. by rewrite big_seq1 big_nil. rewrite (@allpairs_flatten _ _ _ (fun s t => s :: t)) big_flatten big_map /=. rewrite -[X in _ = X](IH (negk k)). 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