[Certora] Delegation invariant

[colin-morpho]

This PR adds the specification for more desired invariants.
These are assumed in other rules so it's good to have them proved to hold.
It uses specification technique suggested by the Certora team. The technique is a bit sophisticated as it involves exhaustively specifying many intermediate properties and using quantificators.

TODO:

• update README;
• ensure the verification succeeds;
• documents the specification.

[QGarchery]

I think it's missing a couple of things to be usable:

• remove the require that sumOfBalances is greater than an account balance
• use the new sumOfBalance definition to show that it's greater than the sum of balances of n accounts (with n = 1 or 2)

The base branch was changed.

[MathisGD]

impressive work!