Prove2Me

lean_workbook_plus_48467

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

if p,qp, q are roots of ax2+bx+cax^2 + bx + c with p>qp > q , then p+q=−b/ap+q = -b/a , pq=c/apq = c/a , and we are given p−q=1p - q = 1 . Eliminating the variables p,qp, q from this system is easy: We have (p+q)2−(p−q)2=4pq,(p+q)^2 - (p-q)^2 = 4pq, consequently b2a2−1=4ca,\frac{b^2}{a^2} - 1 = 4\frac{c}{a}, and since a≠0a \ne 0 , the result follows.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_48467  (a b c p q : ℝ)
  (h₀ : a ≠ 0)
  (h₁ : a * p^2 + b * p + c = 0)
  (h₂ : a * q^2 + b * q + c = 0)
  (h₃ : p > q)
  (h₄ : p - q = 1) :
  p + q = -b / a ∧ p * q = c / a   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph