induction over Intergers

Stream: new members

[mathnoter]

I'm trying to prove the following statement in Lean:

import Mathlib
example (f : ℤ → Prop)
  (h0 : f 0)
  (h1 : ∀ n, f n → f (n + 1))
  (h2 : ∀ n, f n → f (n - 1)) :
  ∀ n, f n := by
    sorry

I am seeking advice on how to approach proving this theorem, specifically regarding how to perform induction over integers (ℤ). I understand how induction works for natural numbers, but I am unsure how to extend this to include negative integers. Any guidance or examples on how to effectively use induction in this context would be greatly appreciated.

Thank you!

[Daniel Weber]

@loogle Int, "induction"

[loogle]

:search: Array.map_induction, Array.mapFinIdx_induction, and 21 more

[Daniel Weber]

You can use docs#Int.induction_on

[Daniel Weber]

Using the induction tactic, this will be induction n using Int.induction_on