Function lemma_decimal4_canonical 

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

requires

pos <= usize::MAX - 2,

pos + 4 <= bytes.len(),

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

ensures

decimal4_bytes(decimal4(bytes, pos))@ == bytes.subrange(pos as int, pos as int + 4),