case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ support (finRotate (2 + m)) = Finset.univ
n : ℕ
h : 2 ≤ n
⊢ support (finRotate n) = Finset.univ
obtain ⟨m, rfl⟩ := exists_add_of_le h
no goals
case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ support (finRotate (2 + m)) = Finset.univ
rw [add_comm, support_finRotate]