∀ {α : Type u_1} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α]
  (isMin : (a : α) → IsMin a → motive a) (succ : (a : α) → ¬IsMax a → motive (Order.succ a))
  (isSuccLimit : (a : α) → Order.IsSuccLimit a → motive a) [inst_2 : NoMaxOrder α] (b : α),
  Order.isSuccLimitRecOn (Order.succ b) isMin succ isSuccLimit = succ b ⋯