Function lemma_der_encodings_sorted_push 

pub proof fn lemma_der_encodings_sorted_push(
    encodings: Seq<Seq<u8>>,
    current: Seq<u8>,
)

requires

der_encodings_sorted(encodings),

ensures

der_encodings_sorted(encodings.push(current))
    <==> (encodings.len() == 0 || der_octets_leq(encodings.last(), current)),

Appending an encoding to a sorted prefix preserves sortedness exactly when it follows the previous last encoding. This uses transitivity of padded DER ordering, so callers only need an adjacent comparison.