rw [orderOf_one]
case inl
G : Type u_1
inst✝ : Group G
h : ∀ (g : G), g = 1 ∨ orderOf g = 2
a b : G
⊢ orderOf 1 ∣ 2
case inl
G : Type u_1
inst✝ : Group G
h : ∀ (g : G), g = 1 ∨ orderOf g = 2
a b : G
⊢ 1 ∣ 2