rw[Nat.le_floor_iff (by linarith)]
case pos.h
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ↑p ≤ z
⊢ 1 ≤ p ∧ p ≤ ⌊z⌋₊
case pos.h
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ↑p ≤ z
⊢ 1 ≤ p ∧ ↑p ≤ z