simp
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∀ (i : ℕ), i ∈ Finset.filter Nat.Prime (Finset.Ioc a b) → i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤ i
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∀ (i : ℕ), a < i → i ≤ b → Nat.Prime i → i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤ i