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