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