have h₁ : 1 < sqrt (2 * x - 1) := by simpa only [← not_le, sqrt_two_mul_sub_one_le_one] using hx
x A : ℝ
hx : 1 < x
⊢ IsGood x A ↔ A = √(4 * x - 2)
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
⊢ IsGood x A ↔ A = √(4 * x - 2)