case H.h
n : ℕ
i : Fin (n + 1)
⊢ ↑(↑(cycleRange (last n)) i) = ↑(↑(finRotate (n + 1)) i)
n : ℕ
⊢ cycleRange (last n) = finRotate (n + 1)
ext i
no goals
case H.h
n : ℕ
i : Fin (n + 1)
⊢ ↑(↑(cycleRange (last n)) i) = ↑(↑(finRotate (n + 1)) i)
rw [coe_cycleRange_of_le (le_last _), coe_finRotate]