Function int_to_be_bytes 

pub open spec fn int_to_be_bytes(v: int) -> Seq<u8>

{
    if v >= 0 {
        nonnegative_int_to_bytes(v as nat)
    } else {
        negative_int_to_bytes((-1 - v) as nat)
    }
}