case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ IsCycle (finRotate (2 + m))
n : ℕ
h : 2 ≤ n
⊢ IsCycle (finRotate n)
obtain ⟨m, rfl⟩ := exists_add_of_le h
case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ IsCycle (finRotate (m + 2))
case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ IsCycle (finRotate (2 + m))
rw [add_comm]
no goals
case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ IsCycle (finRotate (m + 2))
exact isCycle_finRotate