rw [not_le, div_lt_iff_lt_mul' three_pos, mul_comm x] at h2x
case hf
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
x : ℕ
hx : x ≤ 2 * n
h2x : ¬x ≤ 2 * n / 3
⊢ x ^ n.centralBinom.factorization x = 1
case hf
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
⊢ x ^ n.centralBinom.factorization x = 1