Function lemma_to_be_bytes_len_bound 

pub proof fn lemma_to_be_bytes_len_bound(n: nat, max_len: nat)

requires

0 < max_len,

n < pow(256, max_len),

ensures

nat_to_be_bytes(n).len() <= max_len,