chore(data/fintype/fin): add Iio lemmas (#18600)
These are the analogue to the existing `Ioi` lemmas in this file.
`Iio_last_eq_map` is the dual of `Ioi_zero_eq_map`, and `Iio_cast_succ` is the dual of `Ioi_succ`.
I couldn't find a better home for `map_subtype_embedding_univ`.
Note that it is deliberately `subtype_embedding` and not `coe_embedding` to match the similarly-misnamed `fin.map_subtype_embedding_Iio`
