no goals
α : Type u_1
size✝ sz : ℕ
l' : Ordnode α
y : α
r' : Ordnode α
x : α
r : Ordnode α
⊢ dual (eraseMin (node size✝ (node sz l' y r') x r)) = eraseMax (dual (node size✝ (node sz l' y r') x r))
rw [eraseMin, dual_balanceR, dual_eraseMin (node sz l' y r'), dual, dual, dual, eraseMax]