left
case neg
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
⊢ ((x ≤ ↑p ∧ p ≤ ⌊x + y⌋₊) ∧ ∀ (p_1 : ℕ), p_1.Prime → ↑p_1 ≤ z → ¬p_1 ∣ p) ∨ 1 ≤ p ∧ p ≤ ⌊z⌋₊
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
⊢ (x ≤ ↑p ∧ p ≤ ⌊x + y⌋₊) ∧ ∀ (p_1 : ℕ), p_1.Prime → ↑p_1 ≤ z → ¬p_1 ∣ p