case nil
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
h : Sized nil
h_mem : x ∈ nil
⊢ 0 < size nil

case node
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
h : Sized (node size✝ l✝ x✝ r✝)
h_mem : x ∈ node size✝ l✝ x✝ r✝
⊢ 0 < size (node size✝ l✝ x✝ r✝)
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
t : Ordnode α
h : Sized t
h_mem : x ∈ t
⊢ 0 < size t
cases t