proposition: Lemma tdepth1 x (n:= tdepth x): treep x -> [/\ natp n, inc x (tset_index n) & forall m, natp m -> inc x (tset_index m) -> n <=c m].
proof: Proof. move => sa; rewrite /n/tdepth; set U := Zo _ _. have csu: cardinal_set U by move => t /Zo_P [/CS_nat ]. move/tsetP: (sa) => [k ka kb]. have neu: nonempty U by exists k;apply/Zo_P. move: (cle_wor' csu neu); rewrite -/(tdepth x); move => [/Zo_P[sc sd] se]. by split => // m ma mb; apply:se; apply: (Zo_i ma mb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)