Definition octets32BE (n : Z) : list octet := [
  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 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 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 7)
    (bitOf n 6)
    (bitOf n 5)
    (bitOf n 4)
    (bitOf n 3)
    (bitOf n 2)
    (bitOf n 1)
    (bitOf n 0)
].
