∀ {n : ℕ} (hn : Odd n),
  (∀ (a : ZMod n), a + a = 0 ↔ a = 0) →
    ∀ (i j : ZMod n) (h : Commute (DihedralGroup.sr i, DihedralGroup.r j).1 (DihedralGroup.sr i, DihedralGroup.r j).2),
      (fun x =>
            match x with
            | Sum.inl i => ⟨(DihedralGroup.sr i, DihedralGroup.r 0), ⋯⟩
            | Sum.inr (Sum.inl j) => ⟨(DihedralGroup.r 0, DihedralGroup.sr j), ⋯⟩
            | Sum.inr (Sum.inr (Sum.inl k)) =>
              ⟨(DihedralGroup.sr (↑(ZMod.unitOfCoprime 2 ⋯)⁻¹ * k), DihedralGroup.sr (↑(ZMod.unitOfCoprime 2 ⋯)⁻¹ * k)),
                ⋯⟩
            | Sum.inr (Sum.inr (Sum.inr (i, j))) => ⟨(DihedralGroup.r i, DihedralGroup.r j), ⋯⟩)
          ((fun x =>
              match x with
              | ⟨(DihedralGroup.sr i, DihedralGroup.r a), property⟩ => Sum.inl i
              | ⟨(DihedralGroup.r a, DihedralGroup.sr j), property⟩ => Sum.inr (Sum.inl j)
              | ⟨(DihedralGroup.sr i, DihedralGroup.sr j), property⟩ => Sum.inr (Sum.inr (Sum.inl (i + j)))
              | ⟨(DihedralGroup.r i, DihedralGroup.r j), property⟩ => Sum.inr (Sum.inr (Sum.inr (i, j))))
            ⟨(DihedralGroup.sr i, DihedralGroup.r j), h⟩) =
        ⟨(DihedralGroup.sr i, DihedralGroup.r j), h⟩