Function lemma_decimal_scan_characterizes 

pub proof fn lemma_decimal_scan_characterizes(
    bytes: Seq<u8>,
    start: int,
    scanned: int,
)

requires

start == decimal_mantissa_start(bytes),

0 <= start <= scanned <= bytes.len(),

ascii_digits(bytes, start, scanned),

scanned == bytes.len() || !ascii_digit(bytes[scanned]),

ensures

der_real_decimal_wf(bytes) <==> der_real_decimal_at(bytes, scanned),