constructor
case h
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
⊢ ii.val < 7 ∧ a' (N0 + ii.val) = 0
case h.left
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
⊢ ii.val < 7

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
⊢ a' (N0 + ii.val) = 0