/*
*/
showproof: true $

/* 1.1 */
trineq(3*csum(a*b)<=csum(a)^2);
trineq(csum(a)^2<4*csum(a*b));
/* 1.2 */
trineq(csum(a^2)>=(36/35)*(s^2+a*b*c/s));
/* 1.3 */
trineq(8*cprod(s-a)<=a*b*c);
/* 1.4 */
trineq(8*a*b*c<=cprod(a+b));
/* 1.5 */
trineq(3*cprod(a+b)<=8*csum(a^3));
/* 1.6 */
trineq(2*csum(a)*csum(a^2)>=3*(csum(a^3)+3*a*b*c));
/* 1.7 */
trineq(a*b*c<csum(a^2*(s-a)));
trineq(csum(a^2*(s-a))<=3*a*b*c/2);
/* 1.8 */
trineq(csum(a*b*(a+b))>=48*cprod(s-a));
/* 1.9 */
trineq(csum(a^3*(s-a))<=a*b*c*s);
/* 1.10 */
trineq(csum(a^5*(s-a))<=(1/2)*a*b*c*csum(a^3));
/* 1.11 */
/*
trineq(csum(a^2*b*(a-b))>=0);
*/
/* 1.12 */
trineq(64*s^3*cprod(s-a)<=27*a^2*b^2*c^2);
/* 1.14 */
trineq(2*s/(a*b*c)<=csum(1/a^2));
/* 1.15 */
trineq(csum(1/(s-a))>=9/s);
/* 1.16 */
trineq(3/2<=csum(a/(b+c)));
trineq(csum(a/(b+c))<2);
/* 1.17 */
trineq(15/4<=csum((s+a)/(b+c)));
trineq(csum((s+a)/(b+c))<9/2);
/* 1.19 */
trineq(1/3<=csum(a^2)/csum(a)^2);
trineq(csum(a^2)/csum(a)^2<1/2);
/* 1.22 */
trineq(csum(a^2)*csum(b^3*c^3)<2*csum(a^5)*csum(a^3));
/* 1.23 */
trineq(csum(a)^3<=5*csum(a*b*(a+b))-3*a*b*c);

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