pub proof fn lemma_nat_from_base128_bounds(bytes: Seq<u8>)Expand description
ensures
bytes.len() <= 4 ==> nat_from_base128(bytes) <= u32::MAX,bytes.len() <= 9 ==> nat_from_base128(bytes) <= u64::MAX,