mathlib

7aaa53f7 - refactor(order/succ_pred/limit): redefine successor/predecessor limits (#15655)

refactor(order/succ_pred/limit): redefine successor/predecessor limits (#15655) I realized too late that there is a much simpler definition for a successor/predecessor limit (defined in #15001) in terms of the covering relation. We redefine these predicates and port over the existing API. Note that this new definition is only equivalent to the old one in partial orders. The API has remained exactly the same with two caveats: - A few theorems need their assumptions strengthened from preorders to partial orders. - Since `is_succ_limit` is now defined outside of the `order` namespace, all its theorems are moved outside of it too. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>