That makes sense, but this case shows that apparently arbitrary algebraic simplifications aren't allowed because otherwise we could subtract Nat from each side

That makes sense, but this case shows that apparently arbitrary algebraic simplifications aren't allowed because otherwise we could subtract Nat from each side and have trouble.