Function der_octet_at 

pub open spec fn der_octet_at(bytes: Seq<u8>, i: nat) -> u8

{ if i < bytes.len() { bytes[i as int] } else { 0u8 } }

The byte used at i when comparing DER encodings. X.690 §11.6 logically pads the shorter encoding with zero octets at its trailing end.