field_simp
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
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
⊢ (x + √(2 * x - 1)) * 2 = 2 * x - 1 + 2 * √(2 * x - 1) + 1