Theorem octetsBigEndianLengthDivisibleAllExact : forall (b : list bit),
  divisible8 (length b) -> Forall octetIsExact (octetsBigEndian b).
Proof.
  (** Proof omitted for brevity. *)
Qed.
