nat forms a semiring with decidable equality + a total order
most relation between <= and the other operations still TODO