Function der_real_exponent_minimal 

pub open spec fn der_real_exponent_minimal(bytes: Seq<u8>, offset: int, len: int) -> bool

{
    &&& len > 0
    &&& offset >= 0
    &&& offset + len <= bytes.len()
    &&& (len > 1
        ==> {
            &&& !(bytes[offset] == 0x00u8 && bytes[offset + 1] < 0x80u8)
            &&& !(bytes[offset] == 0xffu8 && bytes[offset + 1] >= 0x80u8)

        })

}