Function lemma_decimal_dot_matches_scan 

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

requires

start == decimal_mantissa_start(bytes),

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

ascii_digits(bytes, start, scanned),

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

der_real_decimal_at(bytes, dot),

ensures

dot == scanned,