Use notations like `+?`, `-?`, etc. for scalar binops which can fail

[sonmarcho]

We should keep +, -, etc. for the operations which do not fail, and that would maybe allow automatic coercions from scalars to int/nat when writing specifications.