rw[hp.dvd_iff_eq (hq.ne_one)]
case neg.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
q : ℕ
hq : q.Prime
hqz : ↑q ≤ z
⊢ ¬q ∣ p
case neg.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
q : ℕ
hq : q.Prime
hqz : ↑q ≤ z
⊢ ¬p = q