α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Sized l
hr : Sized r
⊢ Sized (Ordnode.rotateL (Ordnode.dual r) x (Ordnode.dual l))
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Sized l
hr : Sized r
⊢ Sized (Ordnode.dual (Ordnode.rotateR l x r))
rw [dual_rotateR]
no goals
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Sized l
hr : Sized r
⊢ Sized (Ordnode.rotateL (Ordnode.dual r) x (Ordnode.dual l))
exact hr.dual.rotateL hl.dual