proposition: Lemma prod_sin: forall (a b : R), 2 * (sin (a + b) * sin (a - b)) = cos (2 * b) - cos (2 * a).
proof: Proof. intros. assert (cos ((a + b) + (a - b)) = cos (a + b) * cos (a - b) - sin (a + b) * sin (a - b)). rewrite cos_som; auto. assert (cos ((a + b) - (a - b)) = cos (a + b) * cos (a - b) + sin (a + b) * sin (a - b)). rewrite <- cos_diff; auto. assert (2 * (sin (a + b) * sin (a - b)) = cos ((a + b) - (a - b)) - cos ((a + b) + (a - b))). rewrite H0; rewrite H. ring. rewrite H1. RReplace ((a + b) - (a - b)) (2 * b). RReplace ((a + b) + (a - b)) (2 * a); auto. Qed.