Fixpoint octetsBigEndianAux
  (bits   : list bit)
  (octets : list octet)
: list octet :=
  match bits with
  | (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: rest) =>
    octets ++ [OctExact b7 b6 b5 b4 b3 b2 b1 b0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 b4 b3 b2 b1 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 b4 b3 b2 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: b4 :: b3 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 b4 b3 B0 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: b4 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 b4 B0 B0 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 B0 B0 B0 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: rest) =>
    octets ++ [OctRemain b7 b6 B0 B0 B0 B0 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: rest) =>
    octets ++ [OctRemain b7 B0 B0 B0 B0 B0 B0 B0] ++ octetsBigEndianAux rest []
  | [] =>
    octets
  end.
