pub proof fn lemma_to_from_be_bytes_roundtrip(n: nat)Expand description
ensures
nat_from_be_bytes(nat_to_be_bytes(n)) == n,pub proof fn lemma_to_from_be_bytes_roundtrip(n: nat)nat_from_be_bytes(nat_to_be_bytes(n)) == n,