proposition: Lemma Cos_double : forall x : IR, Cos (Two[*]x) [=] Two[*]Cos x[^]2[-][1].
proof: Proof. intros. astepl (Cos (x[+]x)). astepl (Cos x[*]Cos x[-]Sin x[*]Sin x). astepl (Cos x[^]2[-]Sin x[^]2). rstepr (Cos x[^]2[-] ([1][-]Cos x[^]2)). apply cg_minus_wd; algebra. astepr (Cos x[^]2[+]Sin x[^]2[-]Cos x[^]2); rational. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos