This is indeed an interesting approach, but I wonder whether it also allows you to define 'implementations'. Let me explain.
A lot of software development done is because computers are too slow for our demand.[1] It is nice to have an integer type 'nat' that can hold arbitrary large integer numbers (at least as large as fits in the memory model, I presume), but it is not very efficient to use it for every purpose. You also would like to have methods to verify that a certain implementation of a program using a certain 'limited' representation of integers, is correct.