no goals
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Sized l
⊢ size (Ordnode.rotateR l x r) = size l + size r + 1
rw [← size_dual, dual_rotateR, hl.dual.rotateL_size, size_dual, size_dual, add_comm (size l)]