simp at *
case h.succ
x : ℕ × ℕ
n : ℕ
ih : 0 < n → (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[n] x = x → False
hlt : 0 < Nat.succ n
heq : (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[Nat.succ n] x = x
⊢ False
case h.succ
x : ℕ × ℕ
n : ℕ
ih : 0 < n → (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[n] x = x → False
heq :
  (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[n]
      (if x.1 = x.2 then (0, x.2 + 1) else (x.1 + 1, x.2)) =
    x
hlt : True
⊢ False