English
Let α be a linear ordered set with a successor operation and a notion of predecessor prelimits. If b is not a maximum, then the value produced by the successor-prelimit recursion at succ(b) is exactly the successor of b applied to the witness that b is not maximal.
Русский
Пусть α — линейное упорядоченное множество с переходом к следующему элементу и понятием прелимитации предшественников. Если b не предельный максимум, значение функции, задаваемой рекурсией по Succ на succ(b), равноsucc(b, hb).
LaTeX
$$$isSuccPrelimitRecOn(\\mathrm{Order.succ}(b))\\; succ\\; isSuccPrelimit = succ(b, hb),$$$
Lean4
theorem isSuccPrelimitRecOn_succ_of_not_isMax (hb : ¬IsMax b) :
isSuccPrelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b hb :=
by
have hb' := not_isSuccPrelimit_succ_of_not_isMax hb
have H := Classical.choose_spec (not_isSuccPrelimit_iff.1 hb')
rw [isSuccPrelimitRecOn, dif_neg hb', cast_eq_iff_heq]
congr
exacts [(succ_eq_succ_iff_of_not_isMax H.1 hb).1 H.2, proof_irrel_heq _ _]
