Function i32_le_to_bytes 

pub open spec fn i32_le_to_bytes(o: i32) -> [u8; 4]

{ u32_le_to_bytes(o as u32) }