English
If hb is Not IsMin b, then the limitRecOn at (Order.pred b) equals pred b hb (limitRecOn b pred isPredLimit).
Русский
Если hb: Not IsMin(b), то limitRecOn на Order.pred b равен pred b hb (limitRecOn b pred isPredLimit).
LaTeX
$$$\\text{limitRecOn}(\\mathrm{Order.pred}(b)) = \\mathrm{pred}(b)(hb)(\\text{limitRecOn}(b, pred, isPredLimit))$$$
Lean4
theorem limitRecOn_pred_of_not_isMin (hb : ¬IsMin b) :
limitRecOn (Order.pred b) isMax pred isPredLimit = pred b hb (limitRecOn b isMax pred isPredLimit) :=
SuccOrder.limitRecOn_succ_of_not_isMax (α := αᵒᵈ) isMax pred _ hb