proposition: Lemma tree_depth_altE x: treep x -> (tree_depth_alt x) = tdepth x.
proof: Proof. move: x; rewrite /tree_depth_alt;apply: tree_ind. - move => n nN;move: (proj31 (tdepth_prop_inv) _ nN) => [_ ->]. by rewrite tree_recdef_pb //; apply:tset_basei. - move => x xt h; move: (proj32 (tdepth_prop_inv) _ xt) => [sa sb]. by rewrite sb tree_recdef_pp // h. - move => x y xt yt h1 h2; rewrite tree_recdef_px // h1 h2. by move: (proj33 (tdepth_prop_inv) _ _ xt yt) => [_ ->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)