α : Type u_1
r✝ : α → α → Prop
inst✝ : IsStrictOrder α r✝
a : α
r : α → α → Prop
h : ∀ (b : α), ¬Acc r b → ¬r b a
⊢ Acc r a
α : Type u_1
r✝ : α → α → Prop
inst✝ : IsStrictOrder α r✝
a : α
r : α → α → Prop
h : ¬Acc r a
⊢ ∃ b, ¬Acc r b ∧ r b a
contrapose! h
α : Type u_1
r✝ : α → α → Prop
inst✝ : IsStrictOrder α r✝
a : α
r : α → α → Prop
h : ∀ (b : α), ¬Acc r b → ¬r b a
b : α
hr : r b a
⊢ Acc r b
α : Type u_1
r✝ : α → α → Prop
inst✝ : IsStrictOrder α r✝
a : α
r : α → α → Prop
h : ∀ (b : α), ¬Acc r b → ¬r b a
⊢ Acc r a
refine' ⟨_, fun b hr => _⟩
α : Type u_1
r✝ : α → α → Prop
inst✝ : IsStrictOrder α r✝
a : α
r : α → α → Prop
h : ∀ (b : α), ¬Acc r b → ¬r b a
b : α
hr : r b a
hb : ¬Acc r b
⊢ False
α : Type u_1
r✝ : α → α → Prop
inst✝ : IsStrictOrder α r✝
a : α
r : α → α → Prop
h : ∀ (b : α), ¬Acc r b → ¬r b a
b : α
hr : r b a
⊢ Acc r b
by_contra hb
no goals
α : Type u_1
r✝ : α → α → Prop
inst✝ : IsStrictOrder α r✝
a : α
r : α → α → Prop
h : ∀ (b : α), ¬Acc r b → ¬r b a
b : α
hr : r b a
hb : ¬Acc r b
⊢ False
exact h b hb hr