Function lemma_from_to_be_bytes_roundtrip 

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

requires

bytes.len() > 0,

bytes.len() > 1 ==> bytes[0] != 0,

ensures

nat_to_be_bytes(nat_from_be_bytes(bytes)) == bytes,