Cases for impossible values by hypothesis

Stream: new members

[Dominic Steinitz]

I was surprised I had to explicitly do something with 0 as it is ruled out by hypothesis. I assume there is a better way to do this.

example (n : ℕ) (h : n > 0) : n = n - 1 + 1 := by
  cases n with
  | zero => contradiction
  | succ m => rfl

[Luigi Massacci]

Indeed you didn’t have to ; )

[Luigi Massacci]

import Mathlib

example (n : ℕ) (h : n > 0) : n = n - 1 + 1 := by
  cases h with
  | _ => rfl