proposition: Lemma f0_tree l k (t : @tree l k) : 0 <= tree_dist t.
proof: Proof. elim: l k t => [|l IH] k t. by rewrite (tree_frontier t) /= ler01. rewrite (tree_node_children t) /= / tree_dist_children. apply mulr_ge0. by apply LR_pos. rewrite big_map. by apply prodr_ge0. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist