Function lemma_from_base128_upper_bound 

pub proof fn lemma_from_base128_upper_bound(bytes: Seq<u8>)

ensures

nat_from_base128(bytes) < pow(128, bytes.len()),