apply le_of_eq
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₂.h1.a
n : ℕ
hn : 2 < n
⊢ ∏ i in Finset.Ioc (2 * n / 3) n, i ^ ↑(Nat.factorization (Nat.centralBinom n)) i = 1