intro hp
case e_s.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
⊢ p.Prime → (1 ≤ p ∧ p ≤ n ↔ p < n + 1)
case e_s.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
⊢ 1 ≤ p ∧ p ≤ n ↔ p < n + 1