no goals
α : Type ?u.8633
β : Type u_1
inst✝ : CommMonoid β
n : ℕ
f : Fin (n + 1) → β
⊢ ∏ i : Fin (n + 1), f i = (∏ i : Fin n, f (↑castSucc i)) * f (last n)
simpa [mul_comm] using prod_univ_succAbove f (last n)