theorem CoxeterGroup.list_prod_rotate_eq_one {G : Type u_1} [Group G] {w : List G} (hw : w.prod = 1) (k : ℕ) : (w.rotate k).prod = 1

If the product of a list in a group is the identity, then the product of any cyclic rotation of that list is also the identity.