Lean4
/-- Inductively define a function on `ℤ` by defining it at `b`, for the `succ` of a number greater
than `b`, and the `pred` of a number less than `b`. -/
@[elab_as_elim]
protected def inductionOn' : motive z :=
cast (congrArg motive <| show b + (z - b) = z by rw [Int.add_comm, z.sub_add_cancel b]) <|
match z - b with
| .ofNat n => pos n
| .negSucc n => neg n
where
/-- The positive case of `Int.inductionOn'`. -/
pos : ∀ n : ℕ, motive (b + n)
| 0 => cast (by simp) zero
| n + 1 => cast (by rw [Int.add_assoc]; rfl) <| succ _ (Int.le_add_of_nonneg_right (natCast_nonneg _)) (pos n)
/-- The negative case of `Int.inductionOn'`. -/
neg : ∀ n : ℕ, motive (b + -[n+1])
| 0 => pred _ Int.le_rfl zero
| n + 1 => by
refine cast (by cutsat) (pred _ (Int.le_of_lt ?_) (neg n))
cutsat
