本日のC.A.D.

a, b, c がある 3 角形の 3 辺の長さ，ha, hb, hc がその各辺と対頂点との距離（つまり，高さ）ならば

$2(h_a+h_b+h_c)\le\sqrt{3}(a+b+c)$

6.1 Bottema, et. al. "GEOMETRIC INEQUALITIES"

3 角形の面積を d/2 とおくと

? tst12([ex,ex,ex,ex],[x,a,b,c,d],andx,"a<b+c,b<c+a,c<a+b,4*d^2==(a+b+c)*(-a+b+c)*(a-b+c)*(a+b-c),d*(a*b+b*c+c*a)*x==(a+b+c)*a*b*c,0<x");Ans();
 *** using Lazard's method (MPP17).
[d,2]
[c,7]
[b,8]
[a,1]
[x,8]
time = 560 ms.
17 51(0,0) 953(487,174) 613(719,1411) 14(0,28) 
 *** combined adjacent 13 cells.
1[[3*x^2-4,2] <= x,true,true,true,true]
time = 2,840 ms.

? tst12([ex,ex,ex,ex],[x,a,b,c,d],andx,"0<a,a<b+c,b<c+a,c<a+b,4*d^2==(a+b+c)*(-a+b+c)*(a-b+c)*(a+b-c),d*(a*b+b*c+c*a)*x==(a+b+c)*a*b*c,0<x");Ans();
 *** using Lazard's method (MPP17).
[d,2]
[c,7]
[b,8]
[a,1]
[x,8]
time = 543 ms.
17 17(0,0) 451(6,19) 613(249,493) 14(0,28) 
 *** combined adjacent 13 cells.
1[[3*x^2-4,2] <= x,true,true,true,true]
time = 1,503 ms.

? tst12([ex,ex,ex,ex],[x,a,b,c,d],andx,"0<a,0<b,a<b+c,b<c+a,c<a+b,4*d^2==(a+b+c)*(-a+b+c)*(a-b+c)*(a+b-c),d*(a*b+b*c+c*a)*x==(a+b+c)*a*b*c,0<x");Ans();
 *** using Lazard's method (MPP17).
[d,2]
[c,7]
[b,8]
[a,1]
[x,8]
time = 557 ms.
17 17(0,0) 163(6,19) 613(85,136) 14(0,28) 
 *** combined adjacent 13 cells.
1[[3*x^2-4,2] <= x,true,true,true,true]
time = 871 ms.

WLOG 版．

? tst12([ex,ex,ex],[x,b,c,d],andx,"1<b+c,b<c+1,c<1+b,4*d^2==(1+b+c)*(-1+b+c)*(1-b+c)*(1+b-c),d*(b+b*c+c)*x==(1+b+c)*b*c,0<x");Ans()
 *** using Lazard's method (MPP17).
[d,2]
[c,7]
[b,7]
[x,8]
time = 516 ms.
17 451(6,19) 613(249,493) 14(0,28) 
 *** combined adjacent 13 cells.
1[[3*x^2-4,2] <= x,true,true,true]
time = 1,479 ms.

? tst12([ex,ex,ex],[x,b,c,d],andx,"1<=b,b<c+1,c<1+b,4*d^2==(1+b+c)*(-1+b+c)*(1-b+c)*(1+b-c),d*(b+b*c+c)*x==(1+b+c)*b*c,0<x");Ans()
 *** using Lazard's method (MPP17).
[d,2]
[c,7]
[b,7]
[x,8]
time = 515 ms.
17 90(6,19) 334(61,102) 14(0,28) 
 *** combined adjacent 13 cells.
1[[3*x^2-4,2] <= x,true,true,true]
time = 644 ms.

Wolfram Language 12.3.0 Engine for Linux x86 (64-bit)
Copyright 1988-2021 Wolfram Research, Inc.

In[1]:= Reduce[Exists[{a,b,c,d},And[a<b+c,b<c+a,c<a+b,4*d^2==(a+b+c)*(-a+b+c)*(a-b+c)*(a+b-c),d*(a*b+b*c+c*a)*x=
=(a+b+c)*a*b*c,0<x]],Reals]//Timing                                                                             

Out[1]= {549.639162, x >= 2/Sqrt[3]}

In[2]:= Reduce[Exists[{b,c,d},And[1<b+c,b<c+1,c<1+b,4*d^2==(1+b+c)*(-1+b+c)*(1-b+c)*(1+b-c),d*(b+b*c+c)*x==(1+b+
c)*b*c,0<x]],Reals]//Timing                                                                                     

Out[2]= {1.669497, x >= 2/Sqrt[3]}