pub proof fn lemma_from_base128_push(bytes: Seq<u8>, b: u8)Expand description
ensures
nat_from_base128(bytes.push(b)) == nat_from_base128(bytes) * 128 + (b % 128) as nat,