use m
case intro.intro
n : ℕ
hn : 7 ∣ a n
ha' : a' n = 0
m : ℕ
hmgt : n < m
hm7 : a' m = 0
⊢ ∃ M, n < M ∧ 7 ∣ a M
case h
n : ℕ
hn : 7 ∣ a n
ha' : a' n = 0
m : ℕ
hmgt : n < m
hm7 : a' m = 0
⊢ n < m ∧ 7 ∣ a m