Function u16_le_to_bytes 

pub open spec fn u16_le_to_bytes(o: u16) -> [u8; 2]

{ [(o & 0xff) as u8, ((o >> 8) & 0xff) as u8] }