proposition: Lemma Sin_resp_leEq : forall x y, [--] (Pi [/]TwoNZ) [<=] x -> y [<=] Pi [/]TwoNZ -> x [<=] y -> Sin x [<=] Sin y.
proof: Proof. intros; simpl in |- *. cut ( [--] (Pi [/]TwoNZ) [<] Pi [/]TwoNZ). intro H2. apply Derivative_imp_resp_leEq with (clcr [--] (Pi [/]TwoNZ) (Pi [/]TwoNZ)) H2 Cosine; auto. apply Included_imp_Derivative with realline I; Deriv. split; auto; apply leEq_transitive with y; auto. split; auto; apply leEq_transitive with x; auto. intros. apply leEq_glb. intros y0 H3 Hy. apply leEq_wdr with (Cos y0). inversion_clear H3. apply Cos_nonneg. apply leEq_transitive with (Min y x); try apply leEq_Min; auto; apply leEq_transitive with x; auto. apply leEq_transitive with (Max y x); try apply Max_leEq; auto; apply leEq_transitive with y; auto. simpl in |- *; algebra. PiSolve. Qed.
imports: CoRN.transc.Pi CoRN.tactics.CornTac