feat(data/fin): bundled embedding (#3822)
Add the coercion from `fin n` to `ℕ` as a bundled embedding, an
equivalent of `function.embedding.subtype`. Once leanprover-community/lean#359 is fixed
(making `fin n` a subtype), this can go away as a duplicate, but until
then it is useful.
