theorem Hex.PermGroup.Group.hasOrder {n : Nat} (G : Group n) : HasOrder G.generators G.order

The checked group's existing rank and unrank maps witness its order.