Add Pigeon Hole principle.
All threads resolved!
All threads resolved!
Compare changes
- Robbert Krebbers authored
+ 43
− 0
@@ -419,3 +419,46 @@ Section sig_finite.
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.