proposition: Lemma pi_seq_bnd : forall n : nat, pi_seq (S (S (S n))) [-]pi_seq (S (S n)) [<=] ([1][-]Sin [1]) [*] (pi_seq (S (S n)) [-]pi_seq (S n)).
proof: Proof. intros. set (F := FId{+}Cosine) in *. assert (H : Derivative realline I F ( [-C-][1]{+}{--}Sine)). unfold F in |- *; Deriv. astepr ([0][+] ([1][-]Sin [1]) [*] (pi_seq (S (S n)) [-]pi_seq (S n))). apply shift_leEq_plus. apply approach_zero_weak; intros e H0. elim (Law_of_the_Mean _ _ _ _ H (pi_seq (S n)) (pi_seq (S (S n)))) with e. 2: simpl in |- *; auto. 2: simpl in |- *; auto. 2: auto. intros t H1 H2. unfold F in H2. apply leEq_transitive with (pi_seq (S (S (S n))) [-]pi_seq (S (S n)) [-] ([1][-]Sin t) [*] (pi_seq (S (S n)) [-]pi_seq (S n))). unfold cg_minus at 1 5 in |- *; apply plus_resp_leEq_lft. apply inv_resp_leEq. apply mult_resp_leEq_rht. unfold cg_minus in |- *; apply plus_resp_leEq_lft. apply inv_resp_leEq; inversion_clear H1. apply sin_pi_seq_gt_one with (S (S n)). eapply leEq_transitive. 2: apply H3. apply leEq_Min; apply pi_seq_gt_one. eapply leEq_transitive. apply H4. apply Max_leEq; apply less_leEq. eapply less_transitive_unfolded; apply pi_seq_incr. apply pi_seq_incr. apply shift_leEq_minus; apply less_leEq. astepl (pi_seq (S n)); apply pi_seq_incr. eapply leEq_transitive. apply leEq_AbsIR. set (H3 := (I, I)) in *. eapply leEq_wdl. apply (H2 H3 H3 H3). apply AbsIR_wd. Opaque Sine Cosine. simpl in |- *; rational. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos