Function key_fits_at_position 

pub open spec fn key_fits_at_position<Key: Ord, Value>(
    model: CursorMutModel<Key, Value>,
    key: Key,
) -> bool

{
    &&& (model.position == 0 || model.keys[model.position - 1].cmp_spec(&key) is Less)
    &&& (model.position == model.keys.len()
        || key.cmp_spec(&model.keys[model.position]) is Less)

}

Whether a key can be inserted at the cursor’s current gap without breaking key order.