pub proof fn lemma_to_base128_len_bounds()Expand description
ensures
forall |n: u32| #[trigger] nat_to_base128(n as nat).len() <= 5,forall |n: u64| #[trigger] nat_to_base128(n as nat).len() <= 10,