α : Type u_1
inst✝ : Preorder α
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : Valid (node size✝ l x r)
⊢ Valid (eraseMin (node' l x r))
α : Type u_1
inst✝ : Preorder α
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : Valid (node size✝ l x r)
⊢ Valid (eraseMin (node size✝ l x r))
rw [h.2.eq_node']
no goals
α : Type u_1
inst✝ : Preorder α
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : Valid (node size✝ l x r)
⊢ Valid (eraseMin (node' l x r))
exact h.eraseMin_aux.1.valid