Function der_leq 

pub exec fn der_leq(a: &[u8], b: &[u8]) -> leq : bool

ensures

leq == der_octets_leq(a.deep_view(), b.deep_view()),

Executable octet comparison for X.690 §11.6 ordering.