Finished first version of insert'_overflow_leaf_impl_greater_key to help proof insert'_overflow_impl_greater_key