proposition: Lemma Tan_resp_leEq : 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. unfold Tan in |- *. set (H2 := invHalfPi_less_HalfPi) in *. apply Derivative_imp_resp_leEq with (olor [--] (Pi [/]TwoNZ) (Pi [/]TwoNZ)) H2 ( {1/} (Cosine{^}2)). apply Derivative_Tan_1. auto. split; auto; apply leEq_less_trans with y; auto. split; auto; apply less_leEq_trans with x; auto. intros. apply leEq_glb. intros y0 H3 Hy0. cut (Cos y0 [#] [0]). intro H4. apply leEq_wdr with (([1][/] _[//]H4) [^]2). apply sqr_nonneg. simpl in |- *; rational. 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