Lean4
/-- Induction on integers: prove a proposition `p i` by proving the base case `p 0`,
the upwards induction step `p i → p (i + 1)` and the downwards induction step `p (-i) → p (-i - 1)`.
It is used as the default induction principle for the `induction` tactic.
-/
@[elab_as_elim, induction_eliminator]
protected theorem induction_on {motive : ℤ → Prop} (i : ℤ) (zero : motive 0) (succ : ∀ i : ℕ, motive i → motive (i + 1))
(pred : ∀ i : ℕ, motive (-i) → motive (-i - 1)) : motive i := by
cases i with
| ofNat i =>
induction i with
| zero => exact zero
| succ i ih => exact succ _ ih
| negSucc i =>
suffices ∀ n : ℕ, motive (-n) from this (i + 1)
intro n;
induction n with
| zero => simp [zero]
| succ n ih => simpa [natCast_succ, Int.neg_add, Int.sub_eq_add_neg] using pred _ ih
