Function usize_to_be_bytes_in_place 

pub exec fn usize_to_be_bytes_in_place(v: usize, obuf: &mut [u8])

requires

old(obuf)@.len() == nat_to_be_bytes(v as nat).len(),

ensures

final(obuf)@ == nat_to_be_bytes(v as nat),

Writes the minimal big-endian base-256 encoding of v into an exactly-sized slice.