Function u64_to_be_bytes_len 

pub exec fn u64_to_be_bytes_len(v: u64) -> len : usize

requires

usize::BITS == 64,

ensures

len == nat_to_be_bytes(v as nat).len(),