Function lemma_i32_le_value_roundtrip 

pub broadcast proof fn lemma_i32_le_value_roundtrip(o: i32)

ensures

#[trigger] i32_le_from_bytes(i32_le_to_bytes(o)) == o,