ring_nf
x : ℝ
h1 : √31 ^ 2 = 31
⊢ (15 / 8) ^ 2 - (3 - x) * (x + 1) = (x - (1 + √31 / 8)) * (x - (1 - √31 / 8))
x : ℝ
h1 : √31 ^ 2 = 31
⊢ 33 / 64 - x * 2 + x ^ 2 = 1 - x * 2 + x ^ 2 + √31 ^ 2 * (-1 / 64)