have h₂ : x - sqrt (2 * x - 1) = (sqrt (2 * x - 1) - 1) ^ 2 / 2 := by
  rw [sub_sq, sq_sqrt hx']; field_simp; ring
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
⊢ 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
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
h₂ : x - √(2 * x - 1) = (√(2 * x - 1) - 1) ^ 2 / 2
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x