Theorem octetsBigEndianLengthIndivisibleRemainder : ∀ (b : list bit),
  0 < length b mod 8 → ∃ o, In o (octetsBigEndian b) ∧ octetIsRemainder o.
Proof.
  (* Proof omitted for brevity; see ByteOrder.v for proofs. *)
Qed.
