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