Function negative_int_to_bytes 

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

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