This is an unofficial reimagining of the Archive of Formal Proofs
Deriving generic class instances for datatypesby Jonas Rädle and Lars Hupel
Orbit-Stabiliser Theorem with Application to Rotational Symmetriesby Jonas Rädle