proposition: Lemma Sin_One_pos : [0] [<] Sin [1].
proof: Proof. astepl (Sin [0]). simpl in |- *. apply Derivative_imp_resp_less with realline I Cosine. Deriv. apply pos_one. simpl in |- *; auto. simpl in |- *; auto. intros. apply less_leEq_trans with (Cos [1]). apply less_wdr with (Cos (pi_seq 1)). 2: astepl (Cos ([0][+]Cos [0])); apply Cos_wd; Step_final (Cos [0]). apply cos_pi_seq_pos with 1. simpl in |- *. astepr (Cos [0]); astepr OneR. apply less_leEq; apply pos_one. apply leEq_reflexive. apply leEq_glb. intros y H Hy; apply leEq_wdr with (Cos y). 2: simpl in |- *; algebra. inversion_clear H. apply cos_pi_seq_mon with 1. eapply leEq_wdl. apply H0. apply leEq_imp_Min_is_lft; apply less_leEq; apply pos_one. eapply leEq_wdr. apply H1. apply leEq_imp_Max_is_rht; apply less_leEq; apply pos_one. apply eq_imp_leEq; simpl in |- *. Step_final (Cos [0]). Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos