Nat.exists_ne_zero

Stream: Is there code for X?

[Kim Morrison]

Do we have this somewhere?

@[simp] theorem Nat.exists_ne_zero {P : Nat → Prop} : (∃ n, ¬ n = 0 ∧ P n) ↔ ∃ n, P (n + 1) := ...

[Yury G. Kudryashov]

Probably, no.

[Yaël Dillies]

That's one application of the missing Nat.exists + simp afterwards