pub proof fn lemma_usize_to_be_bytes_len_bound(n: usize)Expand description
ensures
usize::BITS == 32 ==> nat_to_be_bytes(n as nat).len() <= 4,usize::BITS == 64 ==> nat_to_be_bytes(n as nat).len() <= 8,