proposition: Lemma tdepth_prop x n: treep x -> natp n -> tdepth x = (csucc n) -> (exists y, [/\ treep y, tdepth y <=c n & x = Tp y]) \/ (exists y z, [/\ treep y, treep z, tdepth y <=c n, tdepth z <=c n & x = Tx y z]).
proof: Proof. move => xt nN dx. move: (proj32 (tdepth1 xt)); rewrite dx (tset_indexS nN); case/tset_nextP. - move => [y ya yb]; constructor 1; exists y; split => //. by apply /tsetP; exists n. by apply:tdepth3. - move => [y [z [ya za ->]]]; constructor 2; exists y,z; split => //. by apply /tsetP; exists n. by apply /tsetP; exists n. by apply:tdepth3. by apply:tdepth3. - by move => h; move:(tdepth3 nN h); rewrite dx => h';case:(cltNge (cltS nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)