rw [← Finset.prod_subset (Finset.Ico_subset_Ico_left (Nat.zero_le a)) _]
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
n a b : ℕ
ha : a ≤ 2
⊢ ∀ (x : ℕ), x ∈ Finset.Ico 0 b → ¬x ∈ Finset.Ico a b → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x = 1