Definition octets16LE (n : Z) : list octet := [
  OctExact
    (bitOf n 7)
    (bitOf n 6)
    (bitOf n 5)
    (bitOf n 4)
    (bitOf n 3)
    (bitOf n 2)
    (bitOf n 1)
    (bitOf n 0);
  OctExact
    (bitOf n 15)
    (bitOf n 14)
    (bitOf n 13)
    (bitOf n 12)
    (bitOf n 11)
    (bitOf n 10)
    (bitOf n 9)
    (bitOf n 8)
].
