Function lemma_base128_fmt_byte_len 

pub proof fn lemma_base128_fmt_byte_len<const MINIMAL: bool>(v: UInt)

ensures

base128_fmt::<MINIMAL>().byte_len(v) == nat_to_base128(v as nat).len(),