proposition: Lemma tree_val_ne n E : (forall i, i <c n -> nonempty (Vg E i)) -> forall t, treep t -> tree_size t <c n -> nonempty(tree_value E t).
proof: Proof. move => hb. apply:tree_ind. + move => i iN. rewrite (proj31 tree_size_p i iN) (proj31 (tree_value_prop E) i iN). by apply: hb. + move => x tx _ _; rewrite (proj32 (tree_value_prop E) _ tx). by exists emptyset; apply: setP_0i. + move => x x' tx tx' hc hd. rewrite(proj33 tree_size_p _ _ tx tx')(proj33 (tree_value_prop E) _ _ tx tx'). move => he. move: (Nmax_p1 (NS_tree_size tx) (NS_tree_size tx')) => [sa sb sc]. move:(rep_i (hc (cle_ltT sb he))); set u := rep _ => e1. move:(rep_i (hd (cle_ltT sc he))); set v := rep _ => e2. by exists (J u v); apply: setXp_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)