Theorem octetsLittleEndianLengthIndivisibleRemainder : forall (b : list bit),
  0 < length b mod 8 -> exists o, In o (octetsLittleEndian b) /\ octetIsRemainder o.
Proof.
  (** Proof omitted for brevity. *)
Qed.
