no goals
α : Type u_1
x✝ : ℕ
l : Ordnode α
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ splitMax' l x (node ls ll lx lr) = (eraseMax (node x✝ l x (node ls ll lx lr)), findMax' x (node ls ll lx lr))
rw [splitMax', splitMax_eq ls ll lx lr, findMax', eraseMax]