Function u64_to_be_bytes_first 

pub exec fn u64_to_be_bytes_first(v: u64) -> first : u8

requires

usize::BITS == 64,

ensures

first == nat_to_be_bytes(v as nat)[0],