Function usize_to_be_bytes_len 

pub exec fn usize_to_be_bytes_len(v: usize) -> len : usize

ensures

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

Executable loop-based byte-length computation. verified against the nat_to_be_bytes specification.