α : Type u_1
t : RBNode α
c : RBColor
n✝ n : Nat
x✝ y✝ : RBNode α
v✝ : α
hl : Balanced x✝ black n
hr : Balanced y✝ black n
⊢ 2 ^ n + 2 ^ n ≤ size x✝ + 1 + (size y✝ + 1)
α : Type u_1
t : RBNode α
c : RBColor
n✝ n : Nat
x✝ y✝ : RBNode α
v✝ : α
hl : Balanced x✝ black n
hr : Balanced y✝ black n
⊢ 2 ^ depthLB red n ≤ size (node red x✝ v✝ y✝) + 1
rw [size, Nat.add_right_comm (size _), Nat.add_assoc, depthLB, Nat.pow_succ, Nat.mul_two]
no goals
α : Type u_1
t : RBNode α
c : RBColor
n✝ n : Nat
x✝ y✝ : RBNode α
v✝ : α
hl : Balanced x✝ black n
hr : Balanced y✝ black n
⊢ 2 ^ n + 2 ^ n ≤ size x✝ + 1 + (size y✝ + 1)
exact Nat.add_le_add hl.le_size hr.le_size
α : Type u_1
t : RBNode α
c : RBColor
n : Nat
x✝ : RBNode α
c₁✝ : RBColor
n✝ : Nat
y✝ : RBNode α
c₂✝ : RBColor
v✝ : α
hl : Balanced x✝ c₁✝ n✝
hr : Balanced y✝ c₂✝ n✝
⊢ 2 ^ n✝ + 2 ^ n✝ ≤ size x✝ + 1 + (size y✝ + 1)
α : Type u_1
t : RBNode α
c : RBColor
n : Nat
x✝ : RBNode α
c₁✝ : RBColor
n✝ : Nat
y✝ : RBNode α
c₂✝ : RBColor
v✝ : α
hl : Balanced x✝ c₁✝ n✝
hr : Balanced y✝ c₂✝ n✝
⊢ 2 ^ depthLB black (n✝ + 1) ≤ size (node black x✝ v✝ y✝) + 1
rw [size, Nat.add_right_comm (size _), Nat.add_assoc, depthLB, Nat.pow_succ, Nat.mul_two]
no goals
α : Type u_1
t : RBNode α
c : RBColor
n : Nat
x✝ : RBNode α
c₁✝ : RBColor
n✝ : Nat
y✝ : RBNode α
c₂✝ : RBColor
v✝ : α
hl : Balanced x✝ c₁✝ n✝
hr : Balanced y✝ c₂✝ n✝
⊢ 2 ^ n✝ + 2 ^ n✝ ≤ size x✝ + 1 + (size y✝ + 1)
refine Nat.add_le_add (Nat.le_trans ?_ hl.le_size) (Nat.le_trans ?_ hr.le_size) <;>
  exact Nat.pow_le_pow_of_le_right (by decide) (depthLB_le ..)
no goals
α : Type u_1
t : RBNode α
c : RBColor
n : Nat
x✝ : RBNode α
c₁✝ : RBColor
n✝ : Nat
y✝ : RBNode α
c₂✝ : RBColor
v✝ : α
hl : Balanced x✝ c₁✝ n✝
hr : Balanced y✝ c₂✝ n✝
⊢ 2 > 0
decide