Theorem octetsLittleEndianLengthDivisibleAllExact : forall (b : list bit),
  divisible8 (length b) -> Forall octetIsExact (octetsLittleEndian b).
Proof.
  (* Proof omitted for brevity; see OctetOrder.v for proofs. *)
Qed.
