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