Function nonnegative_int_to_bytes 

pub open spec fn nonnegative_int_to_bytes(n: nat) -> Seq<u8>

{
    let body = nat_to_be_bytes(n);
    if sign_bit_set(body[0]) { seq![0x00u8] + body } else { body }
}