Function lemma_decimal4_roundtrip 

pub broadcast proof fn lemma_decimal4_roundtrip(value: u16)

requires

value <= 9999,

ensures

digits(#[trigger] decimal4_bytes(value)@, 0, 4),

decimal4(decimal4_bytes(value)@, 0) == value,