Remainders repeat with period seven

Theorem · mod_seven_periodic

Remainders repeat with period seven: $(n + 7) \bmod 7 = n \bmod 7$ .

Formal statement · Lean 4.lean

theorem mod_seven_periodic (n : Nat) : (n + 7) % 7 = n % 7 := by
  sorry

Proof. sorry

Nobody has tried yet.