Access the fact patterns overlap in induction

Stream: new members

[ooovi]

Hi! If my pattern match has overlapping patterns, is there a way to use my knowledge that the current case is none of the previous cases? For example:

import Mathlib.Data.Nat.Defs

def p (n : ℕ) : Bool := sorry

lemma pos : 1 < n → (p n = true) := sorry
lemma zer : p 0 = true := sorry
lemma one : p 1 = true := sorry

lemma all : (n : ℕ) → (p n = true)
| 0 => zer
| 1 => one
| n + 1 => pos _

In the last line, I'd like to have a proof that 1 < n + 1. Is it hiding somewhere?

[Henrik Böving]

I would suggest to match on n + 2 instead