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