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