I have released a new version of IsarMathLib. This time there is some new formalized mathematics related to the theorem that two linearly ordered finite sets with the same number of elements are order-isomorphic and the isomorphism is unique. I have written previously on the motivation for this. The theorem was surprisingly tedious to prove and required about 50 lemmas in a couple of theories. Some corner cases were quite bizarre and kōan-like. For example: what is the order automorphism of the empty set? Turns out the empty set is a function, an injection, surjection, bijection and the only order automorphism of itself.