pub proof fn lemma_from_be_bytes_invert(bytes: Seq<u8>)Expand description
ensures
nat_from_be_bytes(invert_bytes(bytes)) + nat_from_be_bytes(bytes) + 1
== pow(256, bytes.len()),