rw [this, ZMod.natCast_val, ZMod.cast_id', id_def, mul_div_cancel₀ _ hk]
case h.right
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
this : a' (N0 + ii.val) = a' N0 + k * ↑ii.val
⊢ a' (N0 + ii.val) = 0
case h.right
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
this : a' (N0 + ii.val) = a' N0 + k * ↑ii.val
⊢ a' N0 + -a' N0 = 0