Function i16_le_to_bytes 

pub open spec fn i16_le_to_bytes(o: i16) -> [u8; 2]

{ u16_le_to_bytes(o as u16) }