α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
b : BalancedSz (size l) (size r)
bl : Balanced l
br : Balanced r
⊢ BalancedSz (size r) (size l)
α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
b : BalancedSz (size l) (size r)
bl : Balanced l
br : Balanced r
⊢ BalancedSz (size (Ordnode.dual r)) (size (Ordnode.dual l))
rw [size_dual, size_dual]
no goals
α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
b : BalancedSz (size l) (size r)
bl : Balanced l
br : Balanced r
⊢ BalancedSz (size r) (size l)
exact b.symm