Function ber_real_decimal_mantissa_nonzero 

pub open spec fn ber_real_decimal_mantissa_nonzero(
    bytes: Seq<u8>,
    before: nat,
    mark: nat,
    after: nat,
    end: nat,
) -> bool

{
    ||| ascii_digits_have_nonzero(bytes, before as int, mark as int)
    ||| ascii_digits_have_nonzero(bytes, after as int, end as int)

}