I think even better is to have a subtraction that returns a different type, where you can't prove that a > b. Where you can, I don't know that I object to the compiler tracking such things, though I also don't actually use a dependently typed language.