showproof: true $

/* 6.1 */
trineq(2*csum(h(a))<=sqrt(3)*csum(a));
/* 6.4 */
trineq(3*csum(a*b)>=csum(h(a)*h(b)));
/* 6.5 */
trineq(csum(a^3)>(8/7)*csum(h(a)^3));
/* 6.7 */
trineq(csum(a^2/(h(b)^2+h(c)^2))>=2);
/* 6.8 */
trineq(csum(h(a))>=9*r);
/* 6.11 */
trineq(csum(h(a))<=3*(R+r));
/* 6.12 */
trineq(csum(h(a))<=2*R+5*r);
/* 6.13 */
trineq(2*r*(5*R-r)/R<=csum(h(a)));
trineq(csum(h(a))<=2*(R+r)^2/R);
/* 6.15 */
trineq(2*csum(h(a)*h(b))<=6*K*sqrt(3));
trineq(6*K*sqrt(3)<=27*R*r);
/* 6.16 */
trineq(cprod(h(a))>=27*r^3);
/* 6.21 */
trineq(csum(1/(h(a)-2*r))>=3/r);
/* 6.22 */
trineq(csum((h(a)+r)/(h(a)-r))>=6);

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