/*
showproof: true $
*/
showtime:  true $

/* 7.1 */
trineq(K*sqrt(3)<=(R+r)^2);
/* 7.2 */
trineq(K*sqrt(3)<=r*(4*R+r));
/* 7.3 */
trineq(s^2<=4*R^2+(11/(3*sqrt(3)))*K);
/* 7.4 */
trineq(8*R*r+(11/(3*sqrt(3)))*K<=s^2);
/* 7.5 */
trineq(csum(a^2)<=8*R^2+4*K/(3*sqrt(3)));
/* 7.6 */
trineq(csum(a^2)^2<=64*R^4+48*K^2);
/* 7.7 */
trineq(8*K*(2*R-r)<=csum(a^3));
/* 7.8 */
trineq(4*R*(R-4*K/s)^3>=(s^2/4+4*K^2/s^2-2*R^2-5*K*R/s)^2);
/* 7.9 modified */
trineq(4*K<=3*R^2*sqrt(3));
trineq(3*r^2*sqrt(3)<=K);
/* 7.10 */
trineq(r^3*(16*R-5*r)<=K^2);
trineq(K^2<=r^2*(3*r^2+4*R*r+4*R^2));
/* 7.12 */
trineq(9*r/(2*K)<=csum(1/a));
trineq(csum(1/a)<=9*R/(4*K));
/* 7.13 */
trineq(4*R*r+r^2<=K*sqrt(3)+(1/2)*csum((a-b)^2));

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