Function lemma_u16_le_value_roundtrip 

pub broadcast proof fn lemma_u16_le_value_roundtrip(o: u16)

ensures

#[trigger] u16_le_from_bytes(u16_le_to_bytes(o)) == o,