. apply le_of_eq
  apply Finset.prod_eq_one
  intro x hx
  simp at hx
  rw [Nat.factorization_centralBinom_of_two_mul_self_lt_three_mul hn hx.right]
  . simp
  . apply @Nat.lt_of_div_lt_div _ _ 3
    simp
    exact hx.left
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
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