α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
t : Ordset α
h_mem : Ordnode.mem x ↑t = true
⊢ 0 < size t
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
t : Ordset α
h_mem : x ∈ t
⊢ 0 < size t
simp [Membership.mem, mem] at h_mem
no goals
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
t : Ordset α
h_mem : Ordnode.mem x ↑t = true
⊢ 0 < size t
apply Ordnode.pos_size_of_mem t.property.sz h_mem