showHeuristics	=	False;
showproof = True;

triangcount =	0;
triangtrue =	0;

(* 4.2 *)
trineq[s^2>=3K*Sqrt[3]];
(* 4.3 *)
trineq[s^2>=3K*Sqrt[3]+(1/2)*csum[(a-b)^2]];
(* 4.4 *)
trineq[csum[a^2]>=4K*Sqrt[3]];
(* 4.5 *)
trineq[csum[a*b]>=4K*Sqrt[3]];
(* 4.6 *)
trineq[csum[a*b]>=4K*Sqrt[3]+(1/2)*csum[(a-b)^2]];
(* 4.7 *)
trineq[4K*Sqrt[3]+csum[(a-b)^2]<=csum[a^2]];
trineq[csum[a^2]<=4K*Sqrt[3]+3*csum[(a-b)^2]];
(* 4.9 *)
trineq[12K*Sqrt[3]+2*csum[(a-b)^2]<=csum[a]^2];
trineq[csum[a]^2<=12K*Sqrt[3]+8*csum[(a-b)^2]];
(* 4.10 *)
trineq[csum[a^4]>=16K^2];
(* 4.11 *)
trineq[csum[a^4]>=16K^2+4K*csum[(a-b)^2]*Sqrt[3]+(1/2)*csum[(a-b)^2]^2];
(* 4.12 *)
trineq[csum[a^2*b^2]>=16K^2];
(* 4.13 *)
trineq[4K*Sqrt[3]<=9*a*b*c/csum[a]];
(* 4.14 *)
trineq[(a*b*c)^2>=(4K/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<=(4K)^6];

Print[" "];
Print["Summary:"];
Print["Proved ",triangtrue," inequalities out of ",triangcount,"."];