Function lemma_u32_be_value_roundtrip 

pub broadcast proof fn lemma_u32_be_value_roundtrip(o: u32)

ensures

#[trigger] u32_be_from_bytes(u32_be_to_bytes(o)) == o,