Function der_octets_leq 

pub open spec fn der_octets_leq(a: Seq<u8>, b: Seq<u8>) -> bool

{
    if a.len() == 0 && b.len() == 0 {
        true
    } else {
        let left = der_octet_at(a, 0);
        let right = der_octet_at(b, 0);
        ||| left < right
        ||| (left == right
            && der_octets_leq(der_octets_drop_head(a), der_octets_drop_head(b)))

    }
}

Whether complete element encodings are in nondecreasing DER order. Uses the encoded-component ordering from X.690 §11.6.