Theorem octetsLittleEndianLengthDivisibleAllExact : ∀ (b : list bit),
  divisible8 (length b) → Forall octetIsExact (octetsLittleEndian b).
Proof.
  (* Proof omitted for brevity; see ByteOrder.v for proofs. *)
Qed.
