proposition: Lemma sin_pi_seq_gt_one : forall t n, [1] [<=] t -> t [<=] pi_seq (S n) -> Sin [1] [<=] Sin t.
proof: Proof. intros. apply sin_pi_seq_mon with (S n); auto. apply less_leEq; apply pos_one. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos