feat(data/nat/periodic): periodic functions for nat (#10888)
Adds a lemma saying that the cardinality of an Ico of length `a` filtered over a periodic predicate of period `a` is the same as the cardinality of `range a` filtered over that predicate.
Co-authored-by: Johan Commelin <johan@commelin.net>
