I can use Maxima to show that the rhs simplifies to the lhs, but I can't go the other way (except by hand). Any ideas how to force Maxima to derive the rhs from the lhs? Can Mathematica do this? (This is a generalization of sin(2*theta)=2*sin(theta)*cos(theta).) (%i1) sin(x+2*theta)-sin(x) = 2*sin(theta)*cos(x+theta); (%o1) sin(x + 2 theta) - sin(x) = 2 sin(theta) cos(x + theta) (%i2) %,trigexpand,expand; 2 2 (%o2) - sin (theta) sin(x) + cos (theta) sin(x) - sin(x) + 2 cos(theta) sin(theta) cos(x) = 2 cos(theta) sin(theta) cos(x) 2 - 2 sin (theta) sin(x) (%i3) %,trigreduce,expand; (%o3) sin(x + 2 theta) - sin(x) = sin(x + 2 theta) - sin(x)