α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : Sized (node s l x r)
⊢ 0 < size l + size r + 1
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : Sized (node s l x r)
⊢ 0 < s
rw [h.1]
no goals
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : Sized (node s l x r)
⊢ 0 < size l + size r + 1
apply Nat.le_add_left