English
The dual of balance' equals balance' on the duals with appropriate swaps; if certain delta_lt_false cases are considered, the identity holds.
Русский
Дуал balance' равен balance' на дуалах с соответствующими перестановками; при рассмотрении случаев delta_lt_false равенство сохраняется.
LaTeX
$$$$\operatorname{dual}(\operatorname{balance}'(l, x, r)) = \operatorname{balance}'(\operatorname{dual}(r), x, \operatorname{dual}(l)).$$$$
Lean4
theorem dual_balance' (l : Ordnode α) (x : α) (r : Ordnode α) : dual (balance' l x r) = balance' (dual r) x (dual l) :=
by
simp [balance', add_comm]; split_ifs with h h_1 h_2 <;> simp [dual_rotateL, dual_rotateR, add_comm]
cases delta_lt_false h_1 h_2
