theorem Hex.Perm.order_eq_orderOf {n : ℕ} (p : Perm n) : p.order = orderOf p.toEquiv

The executable lcm is the order of the corresponding Mathlib permutation.