Subtype に対してパターンマッチが通るようにしたい

PosNat に対して、n + 1 でパターンマッチができないのか？
何が難しい？難しさもわかっていない。Subtype について、わりと大事な話な気がする。

Zulip: >
pattern match for positive Nat

abbrev PosNat := { x : Nat // x > 0}

@[match_pattern]
def PosNat.add (x y : PosNat) : PosNat :=
  ⟨x.val + y.val, by omega⟩

instance : Add PosNat := ⟨PosNat.add⟩

def PosNat.one : PosNat := ⟨1, by decide⟩

instance : OfNat PosNat 1 := ⟨PosNat.one⟩

def seq (x : PosNat) : ℝ :=
  match x with
  | 1 => 1
  /- invalid patterns, `n` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching
  ⟨.(n.1).succ, ⋯⟩ -/
  | n + 1 => seq n

Start with the PosNat example and the linked Zulip discussion about pattern matching for positive Nat. Investigate how subtype patterns, inaccessible pattern variables, and the n + 1 notation are handled in Lean's pattern-matching implementation. Done would require a decided approach and a documented or tested way for this match to work.