Proving inequalities with Mathematica

Question

Question summary: I would like to learn some tips and tricks on how to prove inequalities with Mathematica.

I'm studying various inequalities in triangle that have the form $R+ar + bs\geq 0$, where $R$ is a circumcircle radius, $r$ is an incircle radius and $s$ is a semiperimeter of a triangle.

ClearAll[R, r, s, isTriangle];
R[x_, y_, z_] := (
 x y z)/Sqrt[(x + y - z) (x - y + z) (-x + y + z) (x + y + z)];
r[x_, y_, z_] := 
  1/2 Sqrt[((x + y - z) (x - y + z) (-x + y + z))/(x + y + z)];
s[x_, y_, z_] := (x + y + z)/2;
isTriangle := 1 >= x > 0 && 1 >= y > 0 && x + y > 1;

I normalize the longest side $z=1$ to simplify the calculation. isTriangle is a condition that there is a triangle with sides $1,x,y$.

I want to prove the following inequalities: $s-3\sqrt{3}r\geq0$ and $-\frac s2+(-2+3\sqrt{3}/2)r+R\geq 0$ for all triangles.

I can easily check that both inequalities are true with the following code:

FindMinimum[{s[1, x, y] - 3 Sqrt[3] r[1, x, y], isTriangle}, {x, y}]

(returns {1.26714*10^-6, {x -> 0.998875, y -> 0.998875}}), i.e. the minimum is $0$);

Resolve[ForAll[{x, y}, isTriangle, 
  s[1, x, y] - 3 Sqrt[3] r[1, x, y] >= 0]]
(* True *)

(checks that inequality holds for all triangles);

FindMinimum[{-s[1, x, y]/2 + (-2 + 3 Sqrt[3]/2) r[1, x, y] + 
   R[1, x, y], isTriangle}, {x, y}]

(returns {9.01882*10^-7, {x -> 0.996601, y -> 0.996601}}, i.e. the minimum is $0$);

Resolve[ForAll[{x, y}, 
  isTriangle, -s[1, x, y]/2 + (-2 + 3 Sqrt[3]/2) r[1, x, y] + 
    R[1, x, y] >= 0]]
(* True *)

(checks that inequality holds for all triangles, but takes some time).

However, I want to find a way to prove them, e.g. so that a human who doesn't trust Mathematica can check that they are always true. I would appreciate some general tips and tricks; e.g. it may be possible to find proves for these particular examples, but I would like to know some (heuristic) methods that could work for some other inequalities, too.

Thanks you very much for your time!