enat.to_with_top
Computably converts an
enat
to a
with_top ℕ
.
enat.with_top_equiv
Order isomorphism between
enat
and
with_top ℕ
.