feat(data/fintype): pigeonhole principles (#4096)
Add pigeonhole principles for finitely and infinitely many pigeons in finitely many holes. There are also strong versions of these, which say that there is a hole containing at least as many pigeons as the average number of pigeons per hole. Fixes #2272.
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
