Commit 2026-07-13 17:10 07c971f2

feat(Order/OrderIsoNat+Data/Finset/Sort): add finiteness and identity theorems for linear orders (#41679) Add theorems to prove that finite, strictly monotone self-maps are the identity. In order to show that we do not lose generality by using the Finite constraint instead of WellFoundedGT + WellFoundedLT add a theorem to prove that a linear order that is well-founded in both directions is finite. To prove the latter also add a theorem to prove that every infinite linear order contains either a strictly increasing or a strictly descreasing sequence. The theorems in Data/Finset/Sort are required for https://github.com/leanprover-community/mathlib4/pull/41160.