rw[h2, ← Nat.add_mod, Nat.mod_mod]
case h
a : ℕ
h : a % 5 < 5
h' : a % 5 ≤ 5
h2 : a % 5 = a % 5 % 5
⊢ (a % 5 + (5 - a % 5) % 5) % 5 = 0
case h
a : ℕ
h : a % 5 < 5
h' : a % 5 ≤ 5
h2 : a % 5 = a % 5 % 5
⊢ (a % 5 + (5 - a % 5)) % 5 = 0