Function lemma_from_be_bytes_lower_bound 

pub proof fn lemma_from_be_bytes_lower_bound(bytes: Seq<u8>)

requires

bytes.len() > 0,

bytes[0] != 0,

ensures

pow(256, (bytes.len() - 1) as nat) <= nat_from_be_bytes(bytes),