Function lemma_integer_from_to_bytes 

pub proof fn lemma_integer_from_to_bytes(i: Seq<u8>)

requires

integer_bytes_wf(i),

ensures

int_to_be_bytes(int_from_be_bytes(i)) == i,