unmatched cases

Stream: mathlib4

[Abhinav Menon]

Hello! I have a function that uses a match on PNat, whose first case is 1. In the second case, I want to have the result that the argument is greater than 1 (using the fact that it would have matched the first case if it was 1). Is this possible?

This is a MWE:

def f (n : PNat) : ℕ :=
  match n with
  | ⟨1, _⟩ => 1
  | ⟨k, h⟩ =>
      let h' : k > 1 := by
        sorry
      5

[Ruben Van de Velde]

Can you write k+2 there?

[Abhinav Menon]

Hmm, wouldn't that give h : k + 2 > 0?

[Abhinav Menon]

Ah, never mind, sorry

[Abhinav Menon]

I see what to do

[Abhinav Menon]

Thank you!