Function lemma_to_base128_props 

pub proof fn lemma_to_base128_props(n: nat)

ensures

nat_to_base128(n).len() > 0,

n > 0 ==> nat_to_base128(n)[0] != 0,

n > 0 ==> pow(128, (nat_to_base128(n).len() - 1) as nat) <= n,

forall |i: int| {
    0 <= i < nat_to_base128(n).len() ==> #[trigger] nat_to_base128(n)[i] < 128
},