no goals
α : Type u_1
x✝ ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
x : α
r : Ordnode α
⊢ splitMin' (node ls ll lx lr) x r = (findMin' (node ls ll lx lr) x, eraseMin (node x✝ (node ls ll lx lr) x r))
rw [splitMin', splitMin_eq ls ll lx lr, findMin', eraseMin]