pub proof fn lemma_from_be_bytes_prepend(bytes: Seq<u8>, b: u8)Expand description
ensures
nat_from_be_bytes(seq![b] + bytes)
== b as nat * pow(256, bytes.len()) + nat_from_be_bytes(bytes),