case a
n : ℕ
a✝ : Fin (n + 2)
⊢ a✝ ∈ support (finRotate (n + 2)) ↔ a✝ ∈ Finset.univ
n : ℕ
⊢ support (finRotate (n + 2)) = Finset.univ
ext
no goals
case a
n : ℕ
a✝ : Fin (n + 2)
⊢ a✝ ∈ support (finRotate (n + 2)) ↔ a✝ ∈ Finset.univ
simp