Interesting article! Given that subtraction isn't closed on the natural numbers, I wonder if it would be possible to implement subtraction as operations on a new type (Integer, Z):

     Z = N x N (Cartesian product or sum type)
     for p, q in Z: p=q if p.first + q.second = q.first + p.second
     p + q := (p.first + q.first, p.second + q.second)
     p - q := (p.first + q.second, p.second + q.first)

Rational numbers can similarly be defined by new operations and equivalence relations on the product set Z x Z. I don't know enough Rust to say whether it's feasible to implement this in the type system, but I'd be curious to hear from someone more experienced!