Adjusted proofs to supply the new assumptions to insert'_overflow_impl_greater_key.