Function lemma_der_octets_leq_step 

pub proof fn lemma_der_octets_leq_step(a: Seq<u8>, b: Seq<u8>)

requires

a.len() > 0 || b.len() > 0,

ensures

der_octet_at(a, 0) < der_octet_at(b, 0) ==> der_octets_leq(a, b),

der_octet_at(a, 0) > der_octet_at(b, 0) ==> !der_octets_leq(a, b),

der_octet_at(a, 0) == der_octet_at(b, 0)
    ==> {
        der_octets_leq(a, b)
            == der_octets_leq(der_octets_drop_head(a), der_octets_drop_head(b))
    },

Expose the one-octet transition used by executable DER cursors.