English
Describes the successor of castAdd m i: it is either natAdd n 0 when i is the last successor, or castAdd of i with its value increased by one, in the non-terminal case.
Русский
Переход succ от castAdd m i равен либо natAdd n 0, если i является последним, либо castAdd с i увеличенным на единицу в противном случае.
LaTeX
$$$$ \\text{succ}(\\operatorname{castAdd} m \\ i) = \\begin{cases} \\operatorname{natAdd} n 0, & \\text{if } i.succ = \\operatorname{last}(n) \\\\ \\operatorname{castAdd}(m+1) \\langle i.1+1, \\; \\text{пояснение}, \\rbrace \\rangle, & \\text{otherwise} \\end{cases} $$$$
Lean4
theorem succ_castAdd (i : Fin n) :
succ (castAdd m i) =
if h : i.succ = last _ then natAdd n (0 : Fin (m + 1))
else castAdd (m + 1) ⟨i.1 + 1, lt_of_le_of_ne i.2 (Fin.val_ne_iff.mpr h)⟩ :=
by
split_ifs with h
exacts [Fin.ext (congr_arg Fin.val h :), rfl]
