apply mulRightLeOfLeOne
case h.h₂.h₂
n : ℕ
hn : 2 < n
⊢ (∏ i in Finset.Ioc (2 * n / 3) n, i ^ ↑(Nat.factorization (Nat.centralBinom n)) i) *
      ∏ i in Finset.Ioc n (2 * n), i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤
    ∏ p in primes (Finset.Ioc n (2 * n)), p
case h.h₂.h₂.h1
n : ℕ
hn : 2 < n
⊢ ∏ i in Finset.Ioc (2 * n / 3) n, i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤ 1

case h.h₂.h₂.h
n : ℕ
hn : 2 < n
⊢ ∏ i in Finset.Ioc n (2 * n), i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤ ∏ p in primes (Finset.Ioc n (2 * n)), p