English
Alternative expression for succ-based limit recursion under not max.
Русский
Альтернативное выражение предел-рекурсии через succ при немаксимум.
LaTeX
$$$\\mathrm{isSuccLimitRecOn}(\\mathrm{Order.succ}(b)) = \\mathrm{succ}(b, hb)$ with $hb: \\neg IsMax(b)$.$$
Lean4
theorem prelimitRecOn_succ_of_not_isMax (hb : ¬IsMax b) :
prelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b hb (prelimitRecOn b succ isSuccPrelimit) :=
by
have h := not_isSuccPrelimit_succ_of_not_isMax hb
have H := Classical.choose_spec (not_isSuccPrelimit_iff.1 h)
rw [prelimitRecOn, WellFounded.fix_eq, dif_neg h]
have {a c : α} {ha hc} {x : ∀ a, motive a} (h : a = c) :
cast (congr_arg (motive ∘ Order.succ) h) (succ a ha (x a)) = succ c hc (x c) := by subst h; rfl
exact this <| (succ_eq_succ_iff_of_not_isMax H.1 hb).1 H.2
