section ‹Basic combinatorics in Isabelle/HOL (and the Archive of Formal Proofs)› theory Combinatorics imports Transposition Stirling Permutations List_Permutation Multiset_Permutations Cycles Perm Orbits begin end