Function ber_real_decimal_significand 

pub open spec fn ber_real_decimal_significand(
    bytes: Seq<u8>,
) -> Option<(nat, nat, nat, nat)>

{
    let before = after_optional_sign(bytes, skip_ascii_spaces(bytes, 1));
    let mark = scan_ascii_digits(bytes, before);
    if mark < bytes.len() && decimal_mark(bytes[mark as int]) {
        let after = mark + 1;
        let end = scan_ascii_digits(bytes, after);
        if before < mark || after < end {
            Some((before, mark, after, end))
        } else {
            None
        }
    } else {
        None
    }
}