proposition: Lemma sin_pi_seq_mon : forall x y n, [0] [<=] x -> x [<=] y -> y [<=] pi_seq n -> Sin x [<=] Sin y.
proof: Proof. intros; simpl in |- *. apply Derivative_imp_resp_leEq with realline I Cosine. Deriv. auto. simpl in |- *; auto. simpl in |- *; auto. intros. apply leEq_glb. intros y0 H2 Hy. apply less_leEq. apply less_wdr with (Cos y0). 2: simpl in |- *; algebra. inversion_clear H2. apply cos_pi_seq_pos with n. apply leEq_transitive with x; auto. eapply leEq_wdl. apply H3. eapply eq_transitive. apply Min_comm. apply leEq_imp_Min_is_lft; auto. apply leEq_transitive with y; auto. eapply leEq_wdr. apply H4. eapply eq_transitive. apply Max_comm. apply leEq_imp_Max_is_rht; auto. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos