Function before_lower_bound 

pub open spec fn before_lower_bound<Key, Q: ?Sized>(key: Key, bound: Bound<&Q>) -> bool

{
    match bound {
        Bound::Included(bound_key) => borrowed_key_cmp(key, bound_key) is Less,
        Bound::Excluded(bound_key) => !(borrowed_key_cmp(key, bound_key) is Greater),
        Bound::Unbounded => false,
    }
}

Whether a key occurs before the gap returned by lower_bound_mut.