intro i
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
this : ∀ (i : ℕ), (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
⊢ IsInfiniteDescendingChain r (descendingChain r z)
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
this : ∀ (i : ℕ), (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
i : ℕ
⊢ r (descendingChain r z (i + 1)) (descendingChain r z i)