α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x x_1 => x > x_1) ↪r r
⊢ Nonempty ((fun x x_1 => x > x_1) ↪r r)
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x x_1 => x > x_1) ↪r r
⊢ ¬WellFounded r
rw [wellFounded_iff_no_descending_seq, not_isEmpty_iff]
no goals
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x x_1 => x > x_1) ↪r r
⊢ Nonempty ((fun x x_1 => x > x_1) ↪r r)
exact ⟨f⟩