Add simplifications for plausible custom overflow criteria

The current program cannot currently be proven by kmir:

pub fn check_checked_add(u1: u64, u2: u64) {
   let result = u1.checked_add(u2);
   if u64::MAX - u2 < u1 {
       assert!(result.is_none());
   } else {
       assert!(result.is_some());
   }
}

The reason is that the overflow criterion used for checked_add is (u1 + u2) & (2^64 - 1) == u1 + u2, and the SMT solver cannot conclude that in this case (2^64 - 1) - u2 < u1 is false.
While the criterion u1.checked_add(u2).is_none() can be used instead in the use case where this comes from, a few suitable lemmas should be added to cover the MAX - .. subtraction way , and other plausible non-standard ways, to check for overflows.

Start with kmir's checked_add overflow criterion and the handling of SMT simplifications. Trace how the existing criterion is encoded, then identify where lemmas for MAX-u2<u1 and other plausible overflow checks belong. Done means the shown check_checked_add example can be proven and the additional non-standard criteria are covered.