apply le_trans (prodLeProdMulProdOfUnionOfOneLe hs (powFactorizationPos _))
case h.h₂
n : ℕ
hn : 2 < n
hs : Finset.Ioc (Nat.sqrt (2 * n)) (2 * n) ⊆ Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3) ∪ Finset.Ioc (2 * n / 3) (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
hs : Finset.Ioc (Nat.sqrt (2 * n)) (2 * n) ⊆ Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3) ∪ Finset.Ioc (2 * n / 3) (2 * n)
⊢ (∏ x in Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x) *
      ∏ x in Finset.Ioc (2 * n / 3) (2 * n), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p