proposition: Lemma sin_3_a: forall (a : R), sin (3 * a) = sin a * (2 * cos (2 * a) + 1).
proof: Proof. intros. RReplace (3 * a) (a + 2 * a). rewrite sin_som. rewrite duplication_sin. RReplace (sin a * cos (2 * a) + (2 * (sin a * cos a)) * cos a) (sin a * (cos (2 * a) + 2 * (cos a * cos a))). assert (2 * Rsqr (cos a) = cos (2 * a) + 1). rewrite duplication_cos. ring. RReplace (cos a * cos a) (Rsqr (cos a)). rewrite H. ring. Qed.