proposition: Lemma pi_seq_Cauchy : Cauchy_prop pi_seq.
proof: Proof. intros e H. cut ([0] [<] pi_seq 2[-]pi_seq 1). intro H0. assert (H1 : pi_seq 2[-]pi_seq 1 [#] [0]). apply Greater_imp_ap; auto. cut (Sin [1] [<] [1]). intro Sin_One_less_One. elim qi_yields_zero with (e := Sin [1][*]e[/] _[//]H1) (q := [1][-]Sin [1]). intros N HN. exists (S (S N)); intros. apply AbsIR_imp_AbsSmall. apply leEq_wdl with (pi_seq m[-]pi_seq (S (S N))). 2: apply eq_symmetric; apply AbsIR_eq_x. 2: apply shift_leEq_minus; astepl (pi_seq (S (S N))). 2: apply local_mon_imp_mon'. 2: intro; apply pi_seq_incr; auto. 2: auto. cut (m = S (pred m)); [ intro | symmetry; apply Nat.lt_succ_pred with (S N); auto ]. apply leEq_wdl with (Sum (S (S N)) (pred m) (fun i : nat => pi_seq (S i) [-]pi_seq i)). 2: eapply eq_transitive. 2: apply Mengolli_Sum_gen with (f := pi_seq). 2: algebra. 2: auto with arith. 2: rewrite <- H3; algebra. set (z := [1][-]Sin [1]) in *. apply leEq_transitive with (Sum (S (S N)) (pred m) (fun i : nat => z[^]pred i[*] (pi_seq 2[-]pi_seq 1))). apply Sum_resp_leEq. rewrite <- H3; auto. intros; apply pi_seq_bnd''. apply Nat.le_trans with (S (S N)); auto with arith. eapply leEq_wdl. 2: apply eq_symmetric; apply Sum_comm_scal with (s := fun i : nat => z[^]pred i). rstepl (Sum (S (S N)) (pred m) (fun i : nat => z[^]pred i) [*] (pi_seq 2[-]pi_seq 1)). apply shift_mult_leEq with H1. auto. apply leEq_wdl with (Sum (S N) (pred (pred m)) (fun i : nat => z[^]i)). 2: cut (pred m = S (pred (pred m))); [ intro | symmetry; apply Nat.lt_succ_pred with N; auto with arith ]. 2: pattern (pred m) at 2 in |- *; rewrite H4. 2: apply Sum_shift; algebra. cut (z[-][1] [#] [0]). intro H4. eapply leEq_wdl. 2: apply eq_symmetric; apply Sum_c_exp with (H := H4). rstepl ((z[^]S (pred (pred m)) [/] _[//]H4) [-] (z[^]S N[/] _[//]H4)). apply leEq_transitive with ( [--] (z[^]S N) [/] _[//]H4). apply shift_minus_leEq; rstepr ZeroR; apply less_leEq. unfold z in |- *. rstepl ( [--] (([1][-]Sin [1]) [^]S (pred (pred m))) [/] Sin [1][//] pos_ap_zero _ _ Sin_One_pos). apply shift_div_less. apply Sin_One_pos. astepr ZeroR; astepr ( [--]ZeroR). apply inv_resp_less. apply less_wdl with (ZeroR[^]S (pred (pred m))). 2: simpl in |- *; algebra. apply nexp_resp_less. auto with arith. apply leEq_reflexive. apply shift_less_minus; astepl (Sin [1]). auto. unfold z at 2 in |- *. rstepl (z[^]S N[/] _[//]pos_ap_zero _ _ Sin_One_pos). apply shift_div_leEq. apply Sin_One_pos. eapply leEq_transitive. eapply leEq_transitive. 2: apply HN. simpl in |- *. astepr (nexp IR N z[*][1]); apply mult_resp_leEq_lft. unfold z in |- *. apply shift_minus_leEq; apply shift_leEq_plus'. astepl ZeroR; apply less_leEq; apply Sin_One_pos. astepr (z[^]N); apply nexp_resp_nonneg. unfold z in |- *. apply shift_leEq_minus; astepl (Sin [1]). apply less_leEq; auto. apply eq_imp_leEq. rational. unfold z in |- *. rstepl ( [--] (Sin [1])). apply inv_resp_ap_zero. apply Greater_imp_ap; apply Sin_One_pos. apply shift_leEq_minus. apply less_leEq; astepl (Sin [1]); auto. apply shift_minus_less; apply shift_less_plus'. astepl ZeroR; apply Sin_One_pos. apply div_resp_pos. auto. apply mult_resp_pos; auto. apply Sin_One_pos. apply Sin_less_One. apply cos_pi_seq_pos with 1. apply less_leEq; apply pos_one. simpl in |- *. apply eq_imp_leEq; Step_final (Cos [0]). apply shift_less_minus; astepl (pi_seq 1). apply pi_seq_incr; auto. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos