#1990 inequality is unknown

[Anonymous]

In 5.21.1, each of the following inequalities are true except the last, which is unknown.

facts();
declare(a,real);
assume(a>0,a<1);
is(a>0);
is(a<1);
is(-a<a);
is(-a/sqrt(a^2+1) < a/sqrt(a^2+1));
is(-(a+1)/sqrt(a^2+1) < (a+1)/sqrt(a^2+1));
is(-(a^2+1)/sqrt(a^2+1) < (a^2+1)/sqrt(a^2+1));
is((-sqrt(a^2+1))/sqrt(a^2+1) < (sqrt(a^2+1))/sqrt(a^2+1));
is((-sqrt(a^2+1)+a)/sqrt(a^2+1) < (sqrt(a^2+1)+a)/sqrt(a^2+1));
is((-2*sqrt(a^2+1)+2*a)/sqrt(a^2+1) < (2*sqrt(a^2+1)+2*a)/sqrt(a^2+1));
is((-2*sqrt(a^2+1)+2*a+2)/sqrt(a^2+1) < (2*sqrt(a^2+1)+2*a+2)/sqrt(a^2+1));