proposition: Lemma tset_min x: treep x -> inc x tset_base \/ exists n, [/\ natp n, inc x (tset_index (csucc n)) & ~inc x (tset_index n)].
proof: Proof. move/tsetP => [n nN ha]. case: (least_int_prop2 nN ha (p := fun t => inc x (tset_index t))). by rewrite tset_index0; left. by set m := cpred _=> j; right; exists m. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)