proposition: Lemma tdepth2 x m: treep x -> natp m -> (tdepth x) <=c m -> inc x (tset_index m).
proof: Proof. move => /tdepth1 [sa sb _] mn le1. rewrite -(cdiff_pr le1). move:(NS_diff (tdepth x) mn); move: (m -c tdepth x); apply: Nat_induction. by rewrite (csum0r (proj31 le1)). move => n nN xa. rewrite (csum_via_succ _ (CS_nat nN)) (tset_indexS (NS_sum sa nN)). by apply/tset_nextP; constructor 3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)