%% The best constants/formulae which belongs to the unit square @var=1
%%
%%
%% input formula QEPCAD
%% 
   (Ex)[ L>1 /\ 0<=x /\ x<=1 /\ -1-2x+x^2>=L(x^2-1) /\ (3-x)<=L(1+x)].
%%
   (Ex)(EL)[ L>1 /\ 5L^2-10L+1<0 /\ 0<=x /\ x<=1 /\ -1-2x+x^2>=L(x^2-1) /\ (3-x)<=L(1+x)].

%% input formula MMA
%%
   Exists[{x},L>1 \[And] (0<x<=1) \[And] -1-2x+x^2>=L(x^2-1) \[And] (3-x)<=L(1+x)]
%%
   Exists[{x,L},L>1 \[And] 5L^2-10L+1<0 \[And] (0<x<=1) \[And] -1-2x+x^2>=L(x^2-1) \[And] (3-x)<=L(1+x)]



%%
%% input formula for pari/gp
 
tst12([ex],[l,x],(f1,f2,f3,f4,f5)->(f1*f2*f3*f4*f5),"l>1, 0<=x, x<=1, (-1-2*x+x^2)>=l*(x^2-1), (3-x)<=l*(1+x)",1) 


%% input formula INTLAB
%%
 
f01a=@(x) max( (3-x)./(1+x),(-1+2*x+x.^2)./(x.^2-1)  

[mu,L,Ls]=verifyglobalmin(f01a,infsup(0,1))


%%OUTPUTS:

L - 1 > 0 /\ 5 L^2 - 10 L + 1 >= 0

Counts for Projection Phase:
------------------------------------------
Level                1         2     Total
------------------------------------------
Proj Poly            7         0         7
Proj Fact            5         4         9
------------------------------------------

Counts for Truth--Invariant CAD Construction Phase:
------------------------------------------
Level                1         2     Total
------------------------------------------
Stacks               1         5         6
..Rational           1         4         5
Cells               11        51        62


 *** using Lazard's method (MPP17).
[x,4]
[l,4]
proj = 71 ms.
5 4(0,4) 
 *** combined adjacent 3 cells.
time = 6 ms.
? Ans();
1[[5*l^2 - 10*l + 1, 2] <= l,true]
? pp
%3 = [[l - 1, l - 3, 5*l^2 - 10*l + 1, l + 1], [x, x - 1, (l - 1)*x^2 + 2*x + (-l + 1), (l + 1)*x + (l - 3)]]