feat(data/nat/count): The count function on naturals (#9457)
feat(data/nat/count): The count function on naturals (#9457)

Defines `nat.count` a generic counting function on `ℕ`, computing how many numbers under `k` satisfy a given predicate".

Co-authored by:
Yaël Dillies, aef64c2b10aaee4bd1b6422c57104205a3c50e06@gmail.com
Vladimir Goryachev, 10c0fbcf88bcfa14c2d3fa000a26c061f9a9f28c@gmail.com
Kyle Miller, 04892e540c93233cb5dfa2674fa5218f82feced5@gmail.com
Scott Morrison, scott@tqft.net
Eric Rodriguez, 58774b6ca42a471874700e44c6b2ee898872147e@gmail.com



Co-authored-by: YaelDillies <aef64c2b10aaee4bd1b6422c57104205a3c50e06@gmail.com>
Co-authored-by: Eric <58774b6ca42a471874700e44c6b2ee898872147e@gmail.com>
Co-authored-by: Kyle Miller <04892e540c93233cb5dfa2674fa5218f82feced5@gmail.com>
Co-authored-by: Vladimir Goryachev <10c0fbcf88bcfa14c2d3fa000a26c061f9a9f28c@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib