feat: implement a natural subtraction which checks that there is no underflow in Lean #747
Description
When using Nat, a - b evaluates to 0 if b > a. This can be confusing and lead to erroneous specifications. It would be good to have a subtraction which requires proving that b <= a.
With regards to syntax, at this stage I believe we shouldn't try to overload - because there will be situations where we can't (or don't want to) prove that b <= a. On the other hand, introducing a special notation is a bit ugly...