I was surprised that we do not have the Pigeon hole principle. It's a trivial consequence of results we already have on Finite types and cardinalities.
