Commit 2026-09-05 15:48 810b3888

feat(Order/OrderIsoNat): every chain is finite when < and > are well-founded (#42633) Also generalizes IsChain.linearOrder from PartialOrder to Preorder. This requires changing the chain hypothesis from ≤ to <, but in a PartialOrder you could use IsChain.lt_of_le to go back (do h.lt_of_le.linearOrder instead of h.linearOrder).