feat(data/finite/basic): `finite` predicate (#14373)
Introduces a `Prop`-valued finiteness predicate on types and adapts some subset of the `fintype` API to get started. Uses `nat.card` as the primary cardinality function.
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
