Definition octetIsRemainder (o : octet): Prop :=
  match o with
  | OctExact  _ _ _ _ _ _ _ _ => False
  | OctRemain _ _ _ _ _ _ _ _ => True
  end.
