Cardinality of sets in constructive mathematics is not as well behaved as in classical mathematics. Cardinalities of finite sets are not natural numbers, and cardinalities are not linearly ordered.
In various mathematical forums, mostly those of a logical flavor, I regularly see people asking basic questions about constructive mathematics. I also see misconceptions about constructive mathematics. I shall make a series of posts, Constructive Gems and Stones, which will answer basic questions about constructive mathematics, and will hopefully help fix wrong ideas about constructive mathematics.
A constructive gem is something nice about constructive mathematics that makes you want to know more about it. In contrast, a constructive stone is a complication in constructive mathematics which does not exist in the classical counterpart.
Here we go! The first one is about finite sets.