proposition: Lemma ET_val1 c i (f := echelon_to_trees c): echelon c -> i <c (slength c) -> P (Vg c i) = \0c -> exists n, Q (Vg c i) = csucc (nat_to_B n) /\ Vg f i = Tree_to_tree (Tbase n).
proof: Proof. move => ha hb az. move: (echelon_to_trees_prop ha) => [_ _ hd hc]. move: (hc _ hb) => [he _ _] {hc}; move: (he az). move => [qa qb qc]. have bN:= (NS_le_nat qb (NS_esize ha)). move: (cpred_pr6' (NS_esize ha) qa qb) => [sa sb sc]. move:(nat_to_B_surjective sa) => [n nv]. by exists n; rewrite /f /= qc {1} sb nv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)