/*
*/
showproof: true $

/* 4.2 */
trineq(s^2>=3*K*sqrt(3));
/* 4.3 */
trineq(s^2>=3*K*sqrt(3)+(1/2)*csum((a-b)^2));
/* 4.4 */
trineq(csum(a^2)>=4*K*sqrt(3));
/* 4.5 */
trineq(csum(a*b)>=4*K*sqrt(3));
/* 4.6 */
trineq(csum(a*b)>=4*K*sqrt(3)+(1/2)*csum((a-b)^2));
/* 4.7 */
trineq(4*K*sqrt(3)+csum((a-b)^2)<=csum(a^2));
trineq(csum(a^2)<=4*K*sqrt(3)+3*csum((a-b)^2));
/* 4.9 */
trineq(12*K*sqrt(3)+2*csum((a-b)^2)<=csum(a)^2);
trineq(csum(a)^2<=12*K*sqrt(3)+8*csum((a-b)^2));
/* 4.10 */
trineq(csum(a^4)>=16*K^2);
/* 4.11 */
trineq(csum(a^4)>=16*K^2+4*K*csum((a-b)^2)*sqrt(3)+(1/2)*csum((a-b)^2)^2);
/* 4.12 */
trineq(csum(a^2*b^2)>=16*K^2);
/* 4.13 */
trineq(4*K*sqrt(3)<=9*a*b*c/csum(a));
/* 4.14 */
trineq((a*b*c)^2>=(4*K/sqrt(3))^3);
/* 4.18 */
trineq((csum(a*b)-csum(a^2)/2)*(3*csum(a*b)-5*csum(a^2)/2)/12<=K^2);
trineq(K^2<=(csum(a*b)-csum(a^2)/2)^2/12);
/* 4.20 */
trineq(27*cprod(b^2+c^2-a^2)^2<=(4*K)^6);

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