α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
⊢ realSize l + Nat.succ (realSize r) = realSize (node size✝ l x✝ r)
α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
⊢ List.length (toList (node size✝ l x✝ r)) = realSize (node size✝ l x✝ r)
rw [toList_node, List.length_append, List.length_cons, length_toList' l,
    length_toList' r]
no goals
α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
⊢ realSize l + Nat.succ (realSize r) = realSize (node size✝ l x✝ r)
rfl