REMIS: The Collins-Johnson Problem
The formula gives necessary and sufficient conditions on the
complex conjugate roots $a \pm bi$ so that there exists a cubic
polynomial with a single real $r$ root in $(0,1)$ yet more than
one variation is obtained.
a1 := -(1-3*r)*(a**2+b**2)+2*a*r;
a2 := -(2-3*r)*(a**2+b**2)+4*a*r-2*a-r;
coj := ex(r,0<r<1 and a>=1/2 and b>0 and a1<0 and a2>0);
Variant from Loos & Weispfenning
lwcoj := ex(r,0<r<1 and a1<0 and a2>0);
end; % of file