have hx' : 0 ≤ 2 * x - 1 := by linarith
case inl
x A : ℝ
hx : 1 / 2 ≤ x
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x