English
The dual of balanceR equals balanceL on the duals: dual (balanceR l x r) = balanceL (dual r) x (dual l).
Русский
Дуал balanceR равен balanceL на дуалах: dual(balanceR(l,x,r)) = balanceL(dual(r)) x (dual(l)).
LaTeX
$$$$\operatorname{dual}(\operatorname{balanceR}(l, x, r)) = \operatorname{balanceL}(\operatorname{dual}(r)) \ x \ (\operatorname{dual}(l)).$$$$
Lean4
theorem dual_balanceR (l : Ordnode α) (x : α) (r : Ordnode α) : dual (balanceR l x r) = balanceL (dual r) x (dual l) :=
by rw [← dual_dual (balanceL _ _ _), dual_balanceL, dual_dual, dual_dual]