case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ cycleType (finRotate (2 + m)) = {2 + m}
n : ℕ
h : 2 ≤ n
⊢ cycleType (finRotate n) = {n}
obtain ⟨m, rfl⟩ := exists_add_of_le h
no goals
case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ cycleType (finRotate (2 + m)) = {2 + m}
rw [add_comm, cycleType_finRotate]