proposition: Lemma pi_seq_incr : forall n : nat, pi_seq n [<] pi_seq (S n).
proof: Proof. intro; astepr (pi_seq n[+]Cos (pi_seq n)). apply shift_less_plus'; astepl ZeroR. apply cos_pi_seq_pos with n. apply pi_seq_nonneg. apply leEq_reflexive. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos