feat(data/nat/nth): add nth function (#10707)
Split off from #9457, introduces `nth` and proves theorems about it.
Co-authored-by: Scott Morrison <scott@tqft.net>
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>
