proposition: Lemma pi_seq_lemma : forall n, [0] [<=] pi_seq n and (forall t : IR, [0] [<=] t -> t [<=] pi_seq n -> [0] [<] Cos t).
proof: Proof. intro; induction n as [| n Hrecn]. split; intros. simpl in |- *; apply leEq_reflexive. simpl in H0. cut (t [=] [0]); [ intro | apply leEq_imp_eq; auto ]. astepr (Cos [0]). astepr OneR. apply pos_one. inversion_clear Hrecn; split. astepr (pi_seq n[+]Cos (pi_seq n)). astepl (ZeroR[+][0]); apply plus_resp_leEq_both. auto. apply less_leEq; apply X; auto. apply leEq_reflexive. simpl in |- *. rename X into H0. intros t H1 H2. apply Continuous_imp_pos with (Hac := leEq_transitive _ _ _ _ H1 H2) (b := pi_seq n); auto. simpl in |- *. apply shift_less_plus'; astepl ZeroR. simpl in H0; apply H0; auto. apply leEq_reflexive. apply included_imp_Continuous with realline; Contin. intros. apply less_wdr with (Cos t0). 2: simpl in |- *; algebra. auto. clear H2 H1 t; intros t H1 H2 Ht. set (x := pi_seq n) in *. apply less_wdr with (Cosine x I[+] ( {--}Cosine x I[-] {--}Cosine t Ht)). 2: simpl in |- *; rational. assert (H3 : Derivative realline I {--}Cosine Sine). apply Derivative_wdr with ( {--}{--}Sine). Opaque Sine. FEQ. Deriv. assert (H4 : Continuous_I (Min_leEq_Max x t) Sine). apply included_imp_Continuous with realline; Contin. set (B := Barrow _ _ Continuous_Sin I {--}Cosine) in *. set (B' := B H3 x t H4 I I) in *. apply less_wdr with (Cosine x I[-]Integral H4). 2: unfold cg_minus at 1 in |- *; apply bin_op_wd_unfolded. 2: algebra. 2: rstepr ( [--] ( {--}Cosine t Ht[-] {--}Cosine x I)). 2: apply un_op_wd_unfolded; eapply eq_transitive. 2: apply B'. 2: algebra. clear B' B H3. apply less_wdl with (Cos (pi_seq n) [-] (pi_seq (S n) [-]pi_seq n)). 2: simpl in |- *; rational. unfold cg_minus at 1 3 in |- *. apply plus_resp_less_lft. apply inv_resp_less. apply less_leEq_trans with (t[-]x). 2: apply minus_resp_leEq; auto. eapply leEq_less_trans. apply leEq_AbsIR. eapply less_leEq_trans. apply (ub_Integral _ _ _ _ H4 (less_imp_ap _ _ _ H1) [1]) with x I. intros. apply leEq_wdl with (AbsIR (Sin x0)). apply AbsIR_Sin_leEq_One. apply AbsIR_wd; simpl in |- *; algebra. apply compact_map2 with (Hab := less_leEq _ _ _ H1). apply compact_inc_lft. apply less_wdl with (AbsIR (Sin x)). 2: simpl in |- *; algebra. apply AbsIR_Sin_less_One. apply H0; auto. apply leEq_reflexive. apply eq_imp_leEq. astepl (AbsIR (t[-]x)). apply AbsIR_eq_x. apply shift_leEq_minus; apply less_leEq. astepl x; auto. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos