Function lemma_decimal2_roundtrip 

pub broadcast proof fn lemma_decimal2_roundtrip(value: u8)

requires

value <= 99,

ensures

digits(#[trigger] decimal2_bytes(value)@, 0, 2),

decimal2(decimal2_bytes(value)@, 0) == value,