rw [Finset.range_eq_Ico]
n a b : ℕ
ha : a ≤ 2
⊢ ∏ p in Finset.range b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p =
    ∏ p in Finset.Ico a b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p
n a b : ℕ
ha : a ≤ 2
⊢ ∏ p in Finset.Ico 0 b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p =
    ∏ p in Finset.Ico a b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p