α : Type u_1
inst✝ : Preorder α
t : Ordnode α
h : Valid t
⊢ Valid (eraseMin (dual t))
α : Type u_1
inst✝ : Preorder α
t : Ordnode α
h : Valid t
⊢ Valid (eraseMax t)
rw [Valid.dual_iff, dual_eraseMax]
no goals
α : Type u_1
inst✝ : Preorder α
t : Ordnode α
h : Valid t
⊢ Valid (eraseMin (dual t))
exact eraseMin.valid h.dual