[Agda] pattern match for LessThan'?

[Kenichi Asai]

In the standard library, we have:

data _≤′_ (m : ℕ) : ℕ → Set where
  ≤′-refl :                         m ≤′ m
  ≤′-step : ∀ {n} (m≤′n : m ≤′ n) → m ≤′ suc n

Suppose we have a value:

v : m ≤′ n

for some m and n.  From the definition of the type, we see that there
must be only one choice for v: if m = n, then v must be refl, while if
m < n, then v must be step.  (And if m > n, v must be ().)

Thus, I want to refine v according to m and n.  Can I do that?  Or in
more general, can I write an inversion function that deconstructs v?
If I case split on v, I always obtain the both possibilities and I
don't see any way to remove the impossible case.

For "less than" without prime:

data _≤_ : Rel ℕ Level.zero where
  z≤n : ∀ {n}                 → zero  ≤ n
  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n

we can simply case split on the value of this type, because the type
uniquely and evidently shows which constructor to take.  I want to do
the same (or similar) thing for "less than" with prime.

Sincerely,

-- 
Kenichi Asai