Lemma mod_8_lt : forall (m : nat),
  0 < (m + 8) mod 8 <-> 0 < m mod 8.
Proof.
  (* Proof omitted for brevity; see OctetOrder.v for proofs. *)
Qed.
