Function lemma_from_be_bytes_push 

pub proof fn lemma_from_be_bytes_push(bytes: Seq<u8>, b: u8)

ensures

nat_from_be_bytes(bytes.push(b)) == nat_from_be_bytes(bytes) * 256 + b as nat,