[Merged by Bors] - feat(Order): Galois connection between pred and succ

[YaelDillies]

This was a longstanding TODO. Kudos to Kevin for putting the pieces together!

---

[github-actions]

PR summary 2056d7f81d

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Order.SuccPred.Basic	341	342	+1 (+0.29%)

Import changes for all files

Files	Import difference
8 files Mathlib.Order.Grade Mathlib.Data.ENat.Basic Mathlib.Order.SuccPred.Basic Mathlib.Data.Nat.SuccPred Mathlib.Order.SuccPred.Relation Mathlib.Order.SuccPred.Limit Mathlib.Data.Fin.SuccPred Mathlib.Data.Int.SuccPred	1

---

Declarations diff

+ WCovBy.covBy_or_le_and_le
+ _
+ _root_.IsMax.of_succ_le
+ _root_.IsMax.succ_le
+ _root_.IsMin.le_pred
+ _root_.IsMin.of_le_pred
+ _root_.LT.lt.le_pred
+ _root_.LT.lt.succ_le
+ gc_pred_succ
+ le_succ_of_wcovBy
+ le_succ_pred
+ pred_eq_of_covBy
+ pred_le_iff_le_succ
+ pred_le_of_wcovBy
+ pred_succ_le
+ succ_eq_of_covBy
- SuccPredOrder

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[kim-em]

Only hesitation is the import increase, otherwise LGTM. Happy if someone wants to merge regardless, or to ask for a split.

[YaelDillies]

As the author of Order.SuccPred.Basic, I claim this import increase is fine 😄

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style