theorem :: SIN_COS:82

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