proposition: Lemma cos_pi_seq_mon : forall x y n, [0] [<=] x -> x [<=] y -> y [<=] pi_seq n -> Cos y [<=] Cos x.
proof: Proof. intros. apply power_cancel_leEq with 2. auto. apply less_leEq; apply cos_pi_seq_pos with n. auto. apply leEq_transitive with y; auto. apply inv_cancel_leEq. rstepl ([1][-]Cos x[^]2[-][1]). rstepr ([1][-]Cos y[^]2[-][1]). apply minus_resp_leEq. apply leEq_wdl with (Sin x[^]2). apply leEq_wdr with (Sin y[^]2). apply nexp_resp_leEq. astepl (Sin [0]); apply sin_pi_seq_mon with n. apply leEq_reflexive. auto. apply leEq_transitive with y; auto. apply sin_pi_seq_mon with n; auto. astepl (Sin y[^]2[+]Cos y[^]2[-]Cos y[^]2). apply cg_minus_wd. Step_final (Cos y[^]2[+]Sin y[^]2). algebra. astepl (Sin x[^]2[+]Cos x[^]2[-]Cos x[^]2). apply cg_minus_wd. Step_final (Cos x[^]2[+]Sin x[^]2). algebra. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos