@[simp]

theorem Real.sqrt_le_self {x : ℝ} : √x ≤ x ↔ x = 0 ∨ 1 ≤ x

@[simp]

theorem Real.le_sqrt_self {x : ℝ} : x ≤ √x ↔ x ≤ 1