have p2nonneg := sq_nonneg (p.2)
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
p1nonneg : 0 ≤ p.1 ^ 2
⊢ p.1 ^ 2 ≤ 1 ∧ p.2 ^ 2 ≤ 1
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
p1nonneg : 0 ≤ p.1 ^ 2
p2nonneg : 0 ≤ p.2 ^ 2
⊢ p.1 ^ 2 ≤ 1 ∧ p.2 ^ 2 ≤ 1