proposition: Lemma cos_som : forall a b : R, cos (a + b) = cos a * cos b + - (sin a * sin b).
proof: Proof. intros. replace (a + b) with (a + - - b). rewrite (cos_diff a (- b)). rewrite cos_paire. rewrite sin_impaire. ring. ring. Qed.