proposition: Lemma pi_seq_bnd'' : forall n : nat, 2 <= n -> pi_seq (S n) [-]pi_seq n [<=] ([1][-]Sin [1]) [^]pred n[*] (pi_seq 2[-]pi_seq 1).
proof: Proof. intro; case n. intros; exfalso; inversion H. clear n. intro; case n; intros. exfalso; inversion H; inversion H1. eapply leEq_wdr. apply pi_seq_bnd'. algebra. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos