proposition: Lemma tree_echelon_s1 x: (treep x /\ tree_size x = \0c) -> echelon_s1 (tree_to_echelon x).
proof: Proof. move => [ha hb]. by move:(tree_to_echelon_ok ha);rewrite hb succ_zero => - [ra [_ /nesym rb] rc]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)