Function lemma_to_base128_len_bound 

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

requires

0 < max_len,

n < pow(128, max_len),

ensures

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