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