obtain rfl | h := h g
G : Type u_1
inst✝ : Group G
h : ∀ (g : G), g = 1 ∨ orderOf g = 2
a b g : G
⊢ orderOf g ∣ 2
case inl
G : Type u_1
inst✝ : Group G
h : ∀ (g : G), g = 1 ∨ orderOf g = 2
a b : G
⊢ orderOf 1 ∣ 2

case inr
G : Type u_1
inst✝ : Group G
h✝ : ∀ (g : G), g = 1 ∨ orderOf g = 2
a b g : G
h : orderOf g = 2
⊢ orderOf g ∣ 2