Given a linearly ordered fintype α of cardinal k, the order isomorphism mono_equiv_of_fin α h is the increasing bijection between fin k and α. Here, h is a proof that the cardinality of α is k. We use this instead of an isomorphism fin (card α) ≃o α to avoid casting issues in further uses of this function.

If α is a linearly ordered fintype, s : finset α has cardinality m and its complement has cardinality n, then fin m ⊕ fin n ≃ α. The equivalence sends elements of fin m to elements of s and elements of fin n to elements of sᶜ while preserving order on each "half" of fin m ⊕ fin n (using set.order_iso_of_fin).