/*
showproof: true $
*/

/* 2.1 */
trineq(csum(sin(A))<=3*sqrt(3)/2);
/* 2.3 */
trineq(csum(sin(A)^2)<=9/4);
/* 2.4 */
trineq(csum(sin(A))>=csum(sin(2*A)));
/* 2.7 */
trineq(cprod(sin(A))<=3*sqrt(3)/8);
/* 2.16 */
trineq(1<csum(cos(A)));
trineq(csum(cos(A))<=3/2);
/* 2.21 */
trineq(3/4<=csum(cos(A)^2));
trineq(csum(cos(A)^2)<3);
/* 2.22 */
trineq(csum(cos(A)*cos(B))<=3/4);
/* 2.23 */
trineq(cprod(cos(A))<=1/8);
/* 2.26 */
trineq(cprod(cos(A))<=(1/24)*csum(cos(A-B)^2));
/* 2.38 */
trineq(csum(cot(A))>=sqrt(3));
/* 2.39 */
trineq(csum(cot(A)^2)>=1);
/* 2.45 */
/* FALSE:
trineq(csum(sec(A))>=6);
*/
/* 2.47 */
/* FALSE
trineq(csum(sec(A)*sec(B))>=12);
*/
/* 2.49 */
trineq(csum(csc(A))>=2*sqrt(3));
/* 2.50 */
trineq(csum(csc(A)^2)>=4);
/* 2.55 */
/* FALSE:
trineq(csum(csc(2*A))>=csum(csc(A)));
*/
/* 2.59 */
trineq((1+cprod(cos(A)))/cprod(sin(A))>=sqrt(3));
/* 2.62 */
trineq(2*csum(cot(A))>=csum(csc(A)));

/* 3.11 */
trineq(-1+4*r/R-(r/R)^2<=csum(cos(A)*cos(B)));
trineq(csum(cos(A)*cos(B))<=r/R+(r/R)^2);
/* 3.13 */
trineq(csum(a*sin(A))>=2*K*sqrt(3)/R);
/* 3.14 */
trineq(9*r<=csum(a*sin(A)));
trineq(csum(a*sin(A))<=9*R/2);
/* 3.15 */
/* sqrt(3) bug
trineq(csum(sin(A))<=2+(3*sqrt(3)-4)*r/R);
*/

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