There is really no need
for derivatives. Here is the answer:
∀a,b,c ∈ ℝ,
[[∃x,y,z ∈ ℝ, ax^2
bx c=ay^2 by c=az^2 bz c=0] ⇒
[(a-b)(b-c)(c-a)=0]].
Note: "(a-b)(b-c)(c-a)=0" is simply the same to
saying "[a=b] ∨ [b=c] ∨ [c=a]", but a few keystrokes shorter.
