Definition octets64LE (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);
  OctExact
    (bitOf n 23)
    (bitOf n 22)
    (bitOf n 21)
    (bitOf n 20)
    (bitOf n 19)
    (bitOf n 18)
    (bitOf n 17)
    (bitOf n 16);
  OctExact
    (bitOf n 31)
    (bitOf n 30)
    (bitOf n 29)
    (bitOf n 28)
    (bitOf n 27)
    (bitOf n 26)
    (bitOf n 25)
    (bitOf n 24);
  OctExact
    (bitOf n 39)
    (bitOf n 38)
    (bitOf n 37)
    (bitOf n 36)
    (bitOf n 35)
    (bitOf n 34)
    (bitOf n 33)
    (bitOf n 32);
  OctExact
    (bitOf n 47)
    (bitOf n 46)
    (bitOf n 45)
    (bitOf n 44)
    (bitOf n 43)
    (bitOf n 42)
    (bitOf n 41)
    (bitOf n 40);
  OctExact
    (bitOf n 55)
    (bitOf n 54)
    (bitOf n 53)
    (bitOf n 52)
    (bitOf n 51)
    (bitOf n 50)
    (bitOf n 49)
    (bitOf n 48);
  OctExact
    (bitOf n 63)
    (bitOf n 62)
    (bitOf n 61)
    (bitOf n 60)
    (bitOf n 59)
    (bitOf n 58)
    (bitOf n 57)
    (bitOf n 56)
].
