inductionOn'_sub_one — Mathlib

Lean4

theorem inductionOn'_sub_one (hz : z ≤ b) :
    (z - 1).inductionOn' b zero succ pred = pred z hz (z.inductionOn' b zero succ pred) :=
  by
  apply cast_eq_iff_heq.mpr
  obtain ⟨n, hn⟩ := Int.eq_negSucc_of_lt_zero (show z - 1 - b < 0 by cutsat)
  rw [hn]
  obtain _ | n := n
  · change _ = -1 at hn
    have : z = b := by omega
    subst this; rw [inductionOn'_self]; exact heq_of_eq rfl
  · have : z = b + -[n+1] := by rw [Int.negSucc_eq] at hn ⊢; omega
    subst this
    refine (cast_heq _ _).trans ?_
    congr
    symm
    rw [Int.inductionOn', cast_eq_iff_heq, show b + -[n+1] - b = -[n+1] by cutsat]

Похожие утверждения