Prove 64 bit integer arithmetics

[jklmnn]

While working on issue #47 I noticed that some properties are harder to prove than expected and are not feasible to prove in the time given. The missing parts are:

• The associativity lemmas for integer conversions between signed and unsigned. Since addition and subtraction are sign-independent the following lemmas are valid but cannot be proven yet (for all ranges):
  • X + Y = To_Int (To_Uns (X) + To_Uns (Y))
  • X - Y = To_Int (To_Uns (X) - To_Uns (Y))
• Multiplication with overflow check is a little more complex than addition and subtraction but it should be provable with moderate effort.
• The division functions are not yet analyzed but after a short overview they're the most complex part of the package and will likely require high effort to prove.