theorem Hex.PermGroup.Group.directProduct_order {n m : Nat} (G : Group n) (H : Group m) : (G.directProduct H).order = G.order * H.order

Unique factor decomposition gives the exact product order. The element lists occur only in this erased proof, never in the product constructor.