English
Dual to eraseMax_aux: removing the minimum element preserves validity and relates sizes appropriately under duality.
Русский
Дуал eraseMax_aux: удаление минимального элемента сохраняет валидность и связывает размеры через двойственность.
LaTeX
$$$\\forall s l x r o_1 o_2,\\; \\mathrm{Valid'} o_1 (\\mathrm{node}~~s~l~x~r) o_2 \\Rightarrow \\mathrm{Valid'} (\\text{WithBot}.some (l.findMin' x)) (l.node' x r).eraseMin o_2 \\land \\mathrm{size}(l.node' x r) = \\mathrm{size}(\\mathrm{eraseMin} (l.node' x r)) + 1$$$
Lean4
theorem eraseMin_aux {s l} {x : α} {r o₁ o₂} (H : Valid' o₁ (.node s l x r) o₂) :
Valid' ↑(findMin' l x) (@eraseMin α (.node' l x r)) o₂ ∧ size (.node' l x r) = size (eraseMin (.node' l x r)) + 1 :=
by
have := H.dual.eraseMax_aux
rwa [← dual_node', size_dual, ← dual_eraseMin, size_dual, ← Valid'.dual_iff, findMax'_dual] at this
