proposition: Lemma Cos_zero : Cos [0] [=] [1].
proof: Proof. simpl in |- *. unfold series_sum in |- *. apply eq_symmetric_unfolded; apply Limits_unique. intros eps H. exists 1; intros. apply AbsSmall_wdr_unfolded with ZeroR. apply zero_AbsSmall; apply less_leEq; auto. simpl in |- *. unfold seq_part_sum in |- *. induction m as [| m Hrecm]. exfalso; inversion H0. clear Hrecm; induction m as [| m Hrecm]. simpl in |- *. unfold cos_seq in |- *. elim even_or_odd_plus; intros; simpl in |- *. elim p; intros; simpl in |- *. cut (x = 0); [ intro | lia ]. rewrite H1; simpl in |- *; rational. exfalso; inversion b. set (n := S m) in *. cut (1 <= n); [ intro | unfold n in |- *; auto with arith ]. cut (n = S m); [ intro | auto ]. clearbody n. simpl in |- *. set (h := fun i : nat => (cos_seq i[/] _[//]nring_fac_ap_zero _ i) [*]nexp IR i ([0][-][0])) in *. fold (h n) in |- *. rstepr (h n[+] (Sum0 n h[-][1])). astepl (ZeroR[+][0]). apply bin_op_wd_unfolded. 2: auto. unfold h, cos_seq in |- *. elim even_or_odd_plus; intros; simpl in |- *. elim p; intros; simpl in |- *. 2: rational. apply eq_symmetric_unfolded; apply x_mult_zero. rewrite H2; simpl in |- *; rational. Qed.
imports: CoRN.transc.TaylorSeries Coq(Lia)