Function lemma_der_octets_leq_transitive 

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

requires

der_octets_leq(a, b),

der_octets_leq(b, c),

ensures

der_octets_leq(a, c),

Padded DER octet ordering is transitive.