Function nat_to_be_bytes 

pub open spec fn nat_to_be_bytes(n: nat) -> Seq<u8>

{
    if n < 256 {
        seq![n as u8]
    } else {
        nat_to_be_bytes((n / 256) as nat).push((n % 256) as u8)
    }
}

Unsigned big-endian base-256 encoding.