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