Function lemma_integer_to_from_bytes 

pub proof fn lemma_integer_to_from_bytes(o: int)

ensures

int_from_be_bytes(int_to_be_bytes(o)) == o,

integer_bytes_wf(int_to_be_bytes(o)),