proposition: Lemma sin_3_a_pisurtrois: forall (a : R), sin (3 * a) = 4 * (sin a * (sin (pisurtrois + a) * sin (pisurtrois - a))).
proof: Proof. intros. rewrite sin_3_a. RReplace (4 * (sin a * (sin (pisurtrois + a) * sin (pisurtrois - a)))) ((2 * sin a) * (2 * (sin (pisurtrois + a) * sin (pisurtrois - a)))). rewrite prod_sin. RReplace ((2 * sin a) * (cos (2 * a) - cos (2 * pisurtrois))) (sin a * (2 * cos (2 * a) - 2 * cos (2 * pisurtrois))). assert (2 * cos (2 * pisurtrois) = - 1). RReplace (- 1) (- 1 + 0). rewrite <- cos_2_pisurtrois. ring. rewrite H. ring. Qed.