∀ {n : ℕ} (motive : DihedralGroup n → DihedralGroup n → Sort u_1) (a b : ZMod n)
  (h_1 : (a b : ZMod n) → motive (DihedralGroup.r a) (DihedralGroup.r b))
  (h_2 : (a a_1 : ZMod n) → motive (DihedralGroup.r a) (DihedralGroup.sr a_1))
  (h_3 : (a a_1 : ZMod n) → motive (DihedralGroup.sr a) (DihedralGroup.r a_1))
  (h_4 : (a b : ZMod n) → motive (DihedralGroup.sr a) (DihedralGroup.sr b)),
  (match DihedralGroup.sr a, DihedralGroup.sr b with
    | DihedralGroup.r a, DihedralGroup.r b => h_1 a b
    | DihedralGroup.r a, DihedralGroup.sr a_1 => h_2 a a_1
    | DihedralGroup.sr a, DihedralGroup.r a_1 => h_3 a a_1
    | DihedralGroup.sr a, DihedralGroup.sr b => h_4 a b) =
    h_4 a b