module PBMatch where

data Nat : Set where
  zz : Nat
  ss : Nat → Nat

_+_ : Nat -> Nat -> Nat
zz + n = n
ss m + n = ss (m + n)

data _<_ : Nat → Nat → Set where
   LE : ∀ {i} → (d : Nat) → i < (d + i)
 
minus : ∀ {m n} → m < n → Nat
minus (LE d) = d

minusSS : ∀ {m n} → m < (ss n) → Nat
minusSS .{ss n}{n} (LE {ss .n} zz) = {!zz!}
minusSS a = ?