proposition: Lemma f1R l : (\sum_(t : @fintree tw l) [ffun x => (@fintree_dist l x)] t = 1).
proof: Proof. under eq_bigr do rewrite ffunE /=. by rewrite f1. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist