proposition: Lemma Sin_double : forall x : IR, Sin (Two[*]x) [=] Two[*]Sin x[*]Cos x.
proof: Proof. intros. astepl (Sin (x[+]x)). eapply eq_transitive_unfolded. apply Sin_plus. rational. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos