proposition: Lemma Sin_zero : Sin [0] [=] [0].
proof: Proof. simpl in |- *. eapply eq_transitive_unfolded. 2: apply (series_sum_zero conv_zero_series). apply series_sum_wd; intros; simpl in |- *. case n. unfold sin_seq in |- *; simpl in |- *. elim even_or_odd_plus; intros; simpl in |- *. elim p; intros; simpl in |- *. rational. exfalso; inversion b. clear n; intro; simpl in |- *. rational. Qed.
imports: CoRN.transc.TaylorSeries Coq(Lia)