Within a fairly weak formal theory of numbers and number-theoretic sequences we give a direct proof of the contrapositive of countable finite choice for decidable predicates. Our proof is at the same time a proof of a stronger form of it. In that way we think that we improve a proof given by Diener and Schuster. Within the same theory we prove properties of inhabited sets of naturals satisfying the general contrapositive of countable choice. Extending our base theory with the continuity principle, we prove that each such set is finite. In that way we generalize a result of Veldman, who proved, actually within the same extension, the finiteness of these sets, supposing additionally their decidability.

constructive mathematics, countable choice