proposition: Lemma ArcTan_range_lemma : {y : IR | olor [--] (Pi [/]TwoNZ) (Pi [/]TwoNZ) y | forall Hy, Tang y Hy [=] x}.
proof: Proof. assert (H : Continuous (olor [--] (Pi [/]TwoNZ) (Pi [/]TwoNZ)) Tang). eapply Derivative_imp_Continuous; apply (Derivative_Tan_1 invHalfPi_less_HalfPi). assert (H0 : Continuous_I (less_leEq _ _ _ ab) Tang). eapply included_imp_Continuous; [ apply H | apply compact_included ]. split; [ apply a1 | apply less_transitive_unfolded with b; [ apply ab | apply b1 ] ]. split; [ apply less_transitive_unfolded with a; [ apply a1 | apply ab ] | apply b1 ]. elim IVT'_I with (contF := H0) (z := x). intros y H1 H2; exists y; auto. inversion_clear H1; split. apply less_transitive_unfolded with a; auto; apply a1. apply less_transitive_unfolded with b; auto; apply b1. apply ab. intros x0 y H1 H2 H3 Hx Hy. fold (Tan x0 Hx) in |- *; fold (Tan y Hy) in |- *. inversion_clear H1; inversion_clear H2; apply Tan_resp_less; auto. apply less_leEq_trans with a; auto; apply a1. apply leEq_less_trans with b; auto; apply b1. fold (Tan a (contin_imp_inc _ _ _ _ H0 _ (compact_inc_lft _ _ _))) in |- *. apply less_leEq_trans with (Tan [--]max max5). apply Tan_resp_less. apply a1. apply less_transitive_unfolded with b; [ apply b5 | apply b1 ]. apply a5. apply max6. fold (Tan b (contin_imp_inc _ _ _ _ H0 _ (compact_inc_rht _ _ _))) in |- *. apply leEq_less_trans with (Tan min min3). apply min4. apply Tan_resp_less. apply min1. apply b1. apply b2. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT