have h' : ∃ f : ℕ → A, f 0 = x ∧ ∀ n, ¬ P (f n) ∧ f n ~> f (n+1) :=
by
  apply (dependent_choice''  (λ a ↦ ¬ P a))
  . exact h
  . intros a npa
    apply Classical.byContradiction
    simp; intros p
    apply npa
    apply IH; intros y ry
    apply Classical.byContradiction; intros npy
    apply (p y npy ry)
case h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
⊢ diverge_from R x
case h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
h' : ∃ f, f 0 = x ∧ ∀ (n : ℕ), ¬P (f n) ∧ R (f n) (f (n + 1))
⊢ diverge_from R x