rw [Real.sq_sqrt hx4, add_left_cancel_iff, Real.sq_sqrt hx5]
x : ℝ
hx4 : 0 ≤ 3 - x
hx5 : 0 ≤ x + 1
⊢ √(3 - x) ^ 2 - 2 * √(3 - x) * √(x + 1) + √(x + 1) ^ 2 = 3 - x - 2 * √(3 - x) * √(x + 1) + (x + 1)
no goals