Function lemma_decimal2_canonical 

pub broadcast proof fn lemma_decimal2_canonical(bytes: Seq<u8>, pos: usize)

requires

pos + 2 <= bytes.len(),

digits(bytes, pos as int, pos as int + 2),

ensures

#[trigger] decimal2_bytes(decimal2(bytes, pos))@
    == bytes.subrange(pos as int, pos as int + 2),