. rw [FactorizationCentralBinom.prodRangePowEqProdIcoPowOfLeTwo (Nat.le_succ _ : 1 ≤ 2)]
  apply le_of_le_of_eq (FactorizationCentralBinom.prodIcoPowLePow' _)
  . norm_num
  . intro hn; rw [hn]; norm_num
case h.h₁
n : ℕ
hn : 2 < n
⊢ ∏ x in Finset.range (Nat.succ (Nat.sqrt (2 * n))), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    (2 * n) ^ Nat.sqrt (2 * n)

case h.h₂
n : ℕ
hn : 2 < n
⊢ ∏ x in Finset.Ioc (Nat.sqrt (2 * n)) (2 * n), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p
case h.h₂
n : ℕ
hn : 2 < n
⊢ ∏ x in Finset.Ioc (Nat.sqrt (2 * n)) (2 * n), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p