A Question about Magic With

I finished preparation for the midterm of Epistemology early, so now I've got time to try to prove that qsort is length-preserving "externally." Given a plain definition of qsort

partition : Nat -> List Nat -> List Nat × List Nat
partition p [] = < [] , [] >
partition p (x :: xs) with partition p xs | cmp x p
... | < ys , zs > | \/-IL x≼p = < x :: ys , zs >
... | < ys , zs > | \/-IR p≼x = < ys , x :: zs >

qsort : List Nat -> List Nat
qsort [] = []
qsort (x :: xs) with partition x xs
... | < ys , zs > = qsort ys ++ x :: qsort zs

the goal is proving

qsort-lenpres : {xs : List Nat} -> EqualLength xs (qsort xs)

I think it is necessary to prove that partition is length-preserving first, so I come up with a function pair-concat that concatenates a pair of lists into one and a proposition partition-lenpres saying that partition is length-preserving.

pair-concat : {A : Set} -> List A × List A -> List A
pair-concat < xs , ys > = xs ++ ys

partition-lenpres : (xs : List Nat)(p : Nat) ->
                      EqualLength xs (pair-concat (partition p xs))

The proof of partition-lenpres is (again) by induction. The base case is trivial.

partition-lenpres [] = eqlen-base

For the inductive case, I asked Agda for the normalised goal type, which is

EqualLength (x :: xs)
(pair-concat (partition p (x :: xs) | cmp x p | partition p xs))

The bars naturally remind me of the "magic with," which is explained on the Agda Wiki and whose usage I never understood before I work on this proof. According to the Agda Wiki, I should write something like

partition-lenpres (x :: xs) p with partition p xs | cmp x p  -- magic with
... | < ys , zs > | \/-IL x≼p = ?0
... | < ys , zs > | \/-IR p≼x = ?1

and the goal types for ?0 and ?1 would simply be EqualLength (x :: xs) (x :: ys ++ zs) and EqualLength (x :: xs) (ys ++ x :: zs) respectively. However when I put the induction hypothesis partition-lenpres {xs}{p} in the place of ?0, the normalised inferred type is

EqualLength xs (pair-concat (partition p xs))

I would expect the innermost partition p xs be replaced by < ys , zs > and the whole type would be further normalised into

EqualLength xs (ys ++ zs)

then the hypothesis term would be a proof for ?0 after an application of eqlen-step. But it doesn't work in that way! Now I cannot construct the desired induction hypothesis and get stuck here.

--
Is there a way to get around?