Function after_optional_sign 

pub open spec fn after_optional_sign(bytes: Seq<u8>, start: nat) -> nat

{
    if start < bytes.len()
        && (bytes[start as int] == ASCII_PLUS || bytes[start as int] == ASCII_MINUS)
    {
        start + 1
    } else {
        start
    }
}