English
If two valid trees can be glued together under a balancedSz condition, then the glued structure is valid and its size equals the sum of parts.
Русский
Если два валидных дерева можно слить (glue) при условии сбалансированности размеров, то слитая структура валидна и ее размер равен сумме размеров частей.
LaTeX
$$$\\forall l\\, r\\, o_1\\, o_2\\; (\\text{ hl },\\text{ hr }, \\text{ bal})\\Rightarrow \\big( \\mathrm{Valid'} o_1 (l.glue r) o_2 \\land \\mathrm{size}(l.glue r) = \\mathrm{size}(l) + \\mathrm{size}(r) \\big) $$$
Lean4
theorem balanceR {l} {x : α} {r o₁ o₂} (hl : Valid' o₁ l x) (hr : Valid' x r o₂)
(H : (∃ l', Raised (size l) l' ∧ BalancedSz l' (size r)) ∨ ∃ r', Raised r' (size r) ∧ BalancedSz (size l) r') :
Valid' o₁ (@balanceR α l x r) o₂ := by rw [Valid'.dual_iff, dual_balanceR];
exact hr.dual.balanceL hl.dual (balance_sz_dual H)
