Amount add and sub now enforce the MAX_MONEY invariant when doing
addition and subtraction. We need to tell kani to assume we don't
overflow before doing actual tests.
Note also that `ops::Add` calls through to `checked_add` and
`ops::Sub` calls through to `checked_sub` so separate kani tests for
these are unnecessary.
Tobin C. Harding