Inductive bitsOctetsHasRemainder : list octet -> Prop :=
  | BOHasRemainder : forall (prefix : list octet) (o : octet),
    Forall octetIsExact prefix ->
      octetIsRemainder o ->
        bitsOctetsHasRemainder (prefix ++ o :: []).
