Function vstd::bytes::spec_u32_to_le_bytes

pub closed spec fn spec_u32_to_le_bytes(x: u32) -> Seq<u8>