[math-fun] An interesting definite integral?

That is similar to "Hard trigonometry integration" at sci.math, 22 Nov 2009 and the elementary solution given by Leon Aigret 22 Nov 2009 (based on the first solution given by Robert Israel, who used residue calculus): f:= x -> cos(2*x)*cos(cos(3*x))^2 = 1/4*cos(2*x-2*cos(3*x))+1/4*cos(2*x+2*cos(3*x))+1/2*cos(2*x) Then (*) f(x) + f(x + 1/3*Pi) + f(x + 2/3*Pi) = 0 using cos(t) + cos (t + 2/3*Pi) + cos (t + 4/3*Pi) = 0. Now observe the function is symmetric w.r.t. Pi/2 and the integral thus is just 1/2 of taking the integral over 0 ... Pi. Then split in 1/3 and 2/3. Transforming the integrals over the last two intervals to live over 0 .. Pi/3 and using (*) gives the assertion, since the over all new integrand simplifies to 0.