∀ {α : Type u_1} (x : α) (x_1 : Ordnode α) (size : ℕ) (ll : Ordnode α) (lx : α) (lr : Ordnode α),
  (Ordnode.node size ll lx lr).splitMin' x x_1 =
    match ll.splitMin' lx lr with
    | (xm, l') => (xm, l'.balanceR x x_1)