Function ber_real_decimal_nr2_wf 

pub open spec fn ber_real_decimal_nr2_wf(bytes: Seq<u8>) -> bool

{
    match ber_real_decimal_significand(bytes) {
        Some((before, mark, after, end)) => (
            &&& end == bytes.len()
            &&& ber_real_decimal_mantissa_nonzero(bytes, before, mark, after, end)

        ),
        None => false,
    }
}