Theorem octetsBigEndianLengthDivisibleNoRemainder : forall (b : list bit),
  Forall octetIsExact (octetsBigEndian b) -> ~bitsOctetsHasRemainder (octetsBigEndian b).
Proof.
  (* Proof omitted for brevity; see OctetOrder.v for proofs. *)
Qed.
