simp_rw [next_apply] at heq
case h
x : ℕ × ℕ
n : ℕ
hlt : 0 < n
heq : next^[n] x = x
⊢ False
case h
x : ℕ × ℕ
n : ℕ
hlt : 0 < n
heq : (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[n] x = x
⊢ False