Definition octetsBigEndian (bits : list bit) : list octet :=
  octetsBigEndianAux bits [].
