feat(data/nat/enat): refactor coe from nat to enat (#9023)
The coercion from nat to enat was defined to be enat.some. But another
coercion could be inferred from the additive structure on enat, leading to
confusing goals of the form
`↑n = ↑n` where the two sides were not defeq.
We now make the coercion inferred from the additive structure the default,
even though it is not computable.
A dedicated function `enat.some` is introduced, to be used whenever
computability is important.
