/*
showproof: true $
*/

/* 5.1 */
trineq(2*r<=R);
/* 5.3 */
trineq(csum(a)<=3*R*sqrt(3));
/* 5.4 */
/* sqrt(3) bug
trineq(s<=2*R+(3*sqrt(3)-4)*r);
*/
/* 5.5 */
trineq(9*r*(4*R+r)<=3*s^2);
trineq(3*s^2<=(4*R+r)^2);
/* 5.6 */
trineq(6*r*(4*R+r)<=2*s^2);
trineq(2*s^2<=2*(2*R+r)^2+R^2);
/* 5.7 */
trineq(2*s^2*(2*R-r)<=R*(4*R+r)^2);
/* 5.8 */
trineq(r*(16*R-5*r)<=s^2);
trineq(s^2<=4*R^2+4*R*r+3*r^2);
/* 5.11 */
trineq(s^2>=27*r^2);
/* 5.12 */
trineq(2*s^2>=27*R*r);
/* 5.13 */
trineq(36*r^2<=csum(a^2));
trineq(csum(a^2)<=9*R^2);
/* 5.14 */
trineq(24*R*r-12*r^2<=csum(a^2));
trineq(csum(a^2)<=8*R^2+4*r^2);
/* 5.16 */
trineq(36*r^2<=csum(a*b));
trineq(csum(a*b)<=9*R^2);
/* 5.17 */
trineq(4*r*(5*R-r)<=csum(a*b));
trineq(csum(a*b)<=4*(R+r)^2);
/* 5.18 */
trineq(36*r^2<=4*r*(5*R-r));
trineq(4*r*(5*R-r)<=csum(a*b));
trineq(4*(R+r)^2<=9*R^2);
/* 5.20 */
trineq(csum(a*(s-a))<=9*R*r);
/* 5.21 */
/* sqrt(3) bug
trineq(a*b*c<=8*R^2*r+(12*sqrt(3)-16)*R*r^2);
*/
/* 5.22 */
trineq(sqrt(3)/R<=csum(1/a));
trineq(csum(1/a)<=sqrt(3)/(2*r));
/* 5.23 */
trineq(3*sqrt(3)/(2*(R+r))<=csum(1/a));
/* 5.24 */
trineq(1/R^2<=csum(1/(a*b)));
trineq(csum(1/(a*b))<=1/(4*r^2));
/* 5.25 */
trineq(8*r*(R-2*r)<=csum((a-b)^2));
trineq(csum((a-b)^2)<=8*R*(R-2*r));
/* 5.26 */
trineq(4*r^2<=a*b*c/csum(a));
/* 5.27 */
trineq(a*b*c<=(R*sqrt(3))^3);
/* 5.33 */
trineq(5*R-r>=s*sqrt(3));
/* 5.36 */
trineq(54*R*r<=3*csum(a*b));

print("Summary:") $
print("Proved",triangtrue,"inequalities out of",triangcount,".") $