English
An advanced version of induction on integers with a shifted base and a successor step: a specific equality expresses how an indexed family propagates under adding one to the index.
Русский
Расширенная индукция по целым числам с переносом через прибавление единицы: равенство описывает поведение семейства по индексу при увеличении на единицу.
LaTeX
$$$$ (hz : z) \\Rightarrow (z + 1).inductionOn' b H_0 H_s H_p = H_s z hz (z.inductionOn' b H_0 H_s H_p) $$$$
Lean4
theorem inductionOn'_add_one (hz : b ≤ z) : (z + 1).inductionOn' b H0 Hs Hp = Hs z hz (z.inductionOn' b H0 Hs Hp) :=
by
apply cast_eq_iff_heq.mpr
lift z - b to ℕ using Int.sub_nonneg.mpr hz with zb hzb
rw [show z + 1 - b = zb + 1 by cutsat]
have : b + zb = z := by omega
subst this
convert cast_heq _ _
rw [Int.inductionOn', cast_eq_iff_heq, ← hzb]
