proposition: Lemma pi_plus_x : forall x : R, cos (pi + x) = - cos x /\ sin (pi + x) = - sin x.
proof: Proof. intros. elim pi_moins_x with (x := - x); intros H H0; try clear pi_moins_x; try exact H0. replace (pi + x) with (pi + - - x). rewrite H0; rewrite H. split; [ try assumption | idtac ]. rewrite cos_paire; auto. rewrite sin_impaire; auto. ring. Qed.