Function lemma_u24_be_value_roundtrip 

pub broadcast proof fn lemma_u24_be_value_roundtrip(o: u32)

requires

o < 0x01000000,

ensures

#[trigger] u24_be_from_bytes(u24_be_to_bytes(o)) == o,