feat(data/nat/fincard): introduce `nat.card`, `enat.card` (#6670)
feat(data/nat/fincard): introduce `nat.card`, `enat.card` (#6670)

Defines `nat`- and `enat`-valued cardinality functions.



Co-authored-by: Aaron Anderson <6a708ae528ec3e8bbcd87cbd53c0d4f4bab63d64@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib