Function lemma_to_be_bytes_props 

pub proof fn lemma_to_be_bytes_props(n: nat)

ensures

nat_to_be_bytes(n).len() > 0,

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

n > 0 ==> pow(256, (nat_to_be_bytes(n).len() - 1) as nat) <= n,