feat(data/nat/enat): new file (#16217) Define enat := with_top nat, use notation.
enat := with_top nat