[condorcet] More precise contract for Sum (avoid overflow)
[condorcet] Attempt at proving no overflow in Sum

* All assertions are individually proved but doing a 'Prove File' on the
  file does not prove everything.
[condorcet] Use two provers for proofs