proposition: Lemma sin_impaire : forall x : R, sin (- x) = - sin x.
proof: Proof. intros. elim pisurdeux_plus_x with (x := - x); intros H H0; try clear pisurdeux_plus_x; try exact H. replace (sin (- x)) with (-1 * - sin (- x)). rewrite <- H. replace (- x + pisurdeux) with (pisurdeux + - x). rewrite <- sin_cos_pisurdeux_moins_x. ring. ring. ring. Qed.