have h1 : Real.sqrt 31 ^ 2 = 31 := Real.sq_sqrt (Nat.ofNat_nonneg _)
x : ℝ
⊢ (15 / 8) ^ 2 - (3 - x) * (x + 1) = (x - (1 + √31 / 8)) * (x - (1 - √31 / 8))
x : ℝ
h1 : √31 ^ 2 = 31
⊢ (15 / 8) ^ 2 - (3 - x) * (x + 1) = (x - (1 + √31 / 8)) * (x - (1 - √31 / 8))