theorem :: SIN_COS:83

for a, b being Real holds cos (a - b) = ((cos a) * (cos b)) + ((sin a) * (sin b))