rw [Nat.succ_le]
case h.left
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 1 ≤ d
case h.left
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 0 < d