Function before_lower_bound 

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

{
    let borrowed_key = <Key as BorrowSpec<Q>>::borrow_spec(&key);
    match bound {
        Bound::Included(bound_key) => borrowed_key.cmp_spec(bound_key) is Less,
        Bound::Excluded(bound_key) => !(borrowed_key.cmp_spec(bound_key) is Greater),
        Bound::Unbounded => false,
    }
}

Whether a key occurs before the gap returned by BTreeMap::lower_bound_mut.