Destructing positive nat

Stream: Is there code for X?

[Joachim Breitner]

Is there a more idiomatic way of writing that first proof line? I have 0 < n and want to replace n with (n + 1):

example (n : Nat) (hpos : 0 < n) (P : Nat → Prop): P n := by
  cases n with | zero => contradiction | succ n =>
  sorry

[Eric Rodriguez]

a terrible way I'm not a real fan of: obtain ⟨n, rfl : _ = n + 1⟩ := Nat.exists_eq_add_of_le' hpos

[Joachim Breitner]

Hmm, I like mine more so far :-D

[Joachim Breitner]

Huh, this works:

example (n : Nat) (hpos : 0 < n) (P : Nat → Prop) (h : ∀ n, P (n+1)): P n := by
  let .succ n := n
  exact h n

What magic is at work here?

[Joachim Breitner]

Ah, missing cases are resolved using something at least as strong as contradiction. Neat!

[Vincent Beffara]

example (n : Nat) (hpos : 0 < n) (P : Nat → Prop) (h : ∀ n, P (n+1)): P n := by
  match n with | n + 1 => exact h n

[Ruben Van de Velde]

obtain \<n, rfl\> := n.exists_eq_succ_of_ne_zero hpos.ne'

[Vincent Beffara]

example (n : Nat) (hpos : 0 < n) (P : Nat → Prop) (h : ∀ n, P (n+1)): P n := by
  cases hpos <;> apply h