I've posted about this a few times but let me try to do so more clearly. How do we, in #constructiveMathematics , show that a set is countably infinite (that is, there is a bijection between our set and the set of natural numbers)? There's a theorem for this which is elegant and also handles some of the trickier cases such as showing that the set of rational numbers is countably infinite. 1/5