α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h₁ : s = size l + size r + 1
h₂ : Sized l
h₃ : Sized r
⊢ realSize l + realSize r + 1 = realSize (node (realSize l + realSize r + 1) l x r)
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h₁ : s = size l + size r + 1
h₂ : Sized l
h₃ : Sized r
⊢ size (node s l x r) = realSize (node s l x r)
rw [size, h₁, size_eq_realSize h₂, size_eq_realSize h₃]
no goals
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h₁ : s = size l + size r + 1
h₂ : Sized l
h₃ : Sized r
⊢ realSize l + realSize r + 1 = realSize (node (realSize l + realSize r + 1) l x r)
rfl