proposition: Lemma f0 l t : 0 <= @fintree_dist l t.
proof: Proof. move: t => [t p1]. rewrite /fintree_dist /=. case: l t {p1} => [|l] /=. move => t. rewrite (tree_frontier t). by apply ler01. move Hs : l.+1.*2 => [ // | [|s]]. by rewrite doubleS in Hs. move=> t. rewrite (tree_node_children t). case Hch: (tree_children t). by apply lexx. rewrite /tree_dist_children. apply mulr_ge0. by apply LR_pos. rewrite big_map. rewrite (big_nth (Node [::])) big_mkord. apply prodr_ge0 => i. by rewrite f0_tree. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist