proposition: Lemma Tan_resp_less : forall x y, [--] (Pi [/]TwoNZ) [<] x -> y [<] Pi [/]TwoNZ -> forall Hx Hy, x [<] y -> Tan x Hx [<] Tan y Hy.
proof: Proof. intros x y H H0 Hx Hy H1. assert (H2 : [--] (Pi [/]TwoNZ) [<] Pi [/]TwoNZ). apply less_transitive_unfolded with x; auto; apply less_transitive_unfolded with y; auto. unfold Tan in |- *. apply Derivative_imp_resp_less with (olor [--] (Pi [/]TwoNZ) (Pi [/]TwoNZ)) H2 ( {1/} (Cosine{^}2)). apply Derivative_Tan_1. auto. split; auto; apply less_transitive_unfolded with y; auto. split; auto; apply less_transitive_unfolded with x; auto. intros. apply less_leEq_trans with OneR. apply pos_one. apply leEq_glb. intros y0 H3 Hy0. cut (Cos y0 [#] [0]). intro H4. apply leEq_wdr with ([1][/] _[//]mult_resp_ap_zero _ _ _ H4 H4). 2: simpl in |- *; rational. apply shift_leEq_div. astepr (Cos y0[^]2); apply pos_square; auto. astepl (Cos y0[*]Cos y0). apply leEq_wdl with (AbsIR (Cos y0) [^]2). astepr (OneR[^]2). apply nexp_resp_leEq. apply AbsIR_nonneg. apply AbsIR_Cos_leEq_One. astepl (AbsIR (Cos y0) [*]AbsIR (Cos y0)). eapply eq_transitive_unfolded. apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply AbsIR_eq_x. astepr (Cos y0[^]2); apply sqr_nonneg. inversion_clear Hy0. apply cring_mult_ap_zero_op with OneR. apply cring_mult_ap_zero with (Cos y0). simpl in |- *; simpl in X0; auto. Qed.
imports: CoRN.transc.Pi CoRN.tactics.CornTac