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, yael.dillies@gmail.com
Vladimir Goryachev, gor050299@gmail.com
Kyle Miller, kmill31415@gmail.com
Scott Morrison, scott@tqft.net
Eric Rodriguez, ericrboidi@gmail.com
Co-authored-by: YaelDillies <yael.dillies@gmail.com>
Co-authored-by: Eric <ericrboidi@gmail.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Vladimir Goryachev <gor050299@gmail.com>
