Function lemma_from_be_bytes_upper_bound 

pub broadcast proof fn lemma_from_be_bytes_upper_bound(bytes: Seq<u8>)

ensures

#[trigger] nat_from_be_bytes(bytes) < pow(256, bytes.len()),