proposition: Lemma pi_seq_bnd' : forall n : nat, pi_seq (S (S (S n))) [-]pi_seq (S (S n)) [<=] ([1][-]Sin [1]) [^]S n[*] (pi_seq 2[-]pi_seq 1).
proof: Proof. intro; induction n as [| n Hrecn]. eapply leEq_wdr. apply pi_seq_bnd. algebra. eapply leEq_transitive. apply pi_seq_bnd. apply leEq_wdr with (([1][-]Sin [1]) [*] (([1][-]Sin [1]) [^]S n[*] (pi_seq 2[-]pi_seq 1))). 2: simpl in |- *; rational. apply mult_resp_leEq_lft. auto. apply shift_leEq_minus; astepl (Sin [1]). eapply leEq_transitive. apply leEq_AbsIR. apply AbsIR_Sin_leEq_One. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos