proposition: Lemma tree_to_echelon_ok t (c := tree_to_echelon t): treep t -> [/\ echelon c, \0c <c slength c & esize c = csucc (tree_size t)].
proof: Proof. rewrite /c{c}; move:t; apply: tree_ind. - move => n nN. move: (Ech_base_prop (NS_succ nN) (succ_positive n)) => [ea eb ec ed]. rewrite (proj31 tree_to_echelon_E _ nN); split => //. by rewrite ed (proj31 tree_size_p _ nN). - move => x tx [h1 h2 h3]. move:(Ech_powerset_prop h1 h2); rewrite h3; move => [ha hb hc _ _]. rewrite (proj32 tree_to_echelon_E _ tx) hc (proj32 tree_size_p _ tx) hb. split => //; apply: succ_positive. - move => x x' tx tx' [h1 h2 h3] [h1' h2' h3']. rewrite (proj33 tree_to_echelon_E _ _ tx tx') (proj33 tree_size_p _ _ tx tx'). move:(Ech_product_prop h1 h1' h2) => [ra rb rc _]; rewrite rc;split => //. by rewrite rb; apply: succ_positive. by rewrite h3 h3' cmax_succ //;apply: CS_nat; apply:NS_tree_size. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)