proposition: Lemma Tan_zero : forall H, Tan [0] H [=] [0].
proof: Proof. intros; unfold Tan, Tang in |- *. simpl in |- *. astepr (ZeroR [/]OneNZ); apply div_wd. astepr (Sin [0]); simpl in |- *; algebra. astepr (Cos [0]); simpl in |- *; algebra. Qed.
imports: CoRN.transc.TaylorSeries Coq(Lia)