proposition: Lemma sin_som : forall a b : R, sin (a + b) = sin a * cos b + sin b * cos a.
proof: Proof. intros. replace (sin (a + b)) with (cos (pisurdeux + - (a + b))). replace (pisurdeux + - (a + b)) with (pisurdeux + - a + - b). rewrite cos_diff. rewrite <- sin_cos_pisurdeux_moins_x. rewrite <- cos_sin_pisurdeux_moins_x. ring. ring. rewrite <- sin_cos_pisurdeux_moins_x; auto. Qed.