rw [add_sq, sq_sqrt hx']
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
⊢ x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
⊢ x + √(2 * x - 1) = (2 * x - 1 + 2 * √(2 * x - 1) * 1 + 1 ^ 2) / 2