proposition: Lemma maps_Tan : maps_compacts_into (olor [--] (Pi [/]TwoNZ) (Pi [/]TwoNZ)) realline Tang.
proof: Proof. intros a b Hab H. elim (H _ (compact_inc_lft _ _ Hab)); intros Ha1 Ha2. elim (H _ (compact_inc_rht _ _ Hab)); intros Hb1 Hb2. cut (Dom Tang b). cut (Dom Tang a). intros H0 H1. set (min := Min (Tan a H0) [0]) in *. set (max := Max (Tan b H1) [1]) in *. cut (min [<] max). intro H2. exists min; exists max; exists H2. split. Included. intros x Hx H3. fold (Tan x Hx) in |- *. unfold Nat.min, Nat.max in |- *; inversion_clear H3. split. eapply leEq_transitive; [ apply Min_leEq_lft | apply Tan_resp_leEq; auto ]. apply leEq_less_trans with b; auto. eapply leEq_transitive. 2: apply lft_leEq_Max. apply Tan_resp_leEq; auto. apply less_leEq_trans with a; auto. unfold Nat.min, Nat.max in |- *. eapply leEq_less_trans. apply Min_leEq_rht. eapply less_leEq_trans; [ apply pos_one | apply rht_leEq_Max ]. split. apply sin_domain. split. apply cos_domain. intros; apply ap_wdl with (Cos a). apply Greater_imp_ap; apply Cos_pos; auto. simpl in |- *; algebra. split. apply sin_domain. split. apply cos_domain. intros; apply ap_wdl with (Cos b). apply Greater_imp_ap; apply Cos_pos; auto. simpl in |- *; algebra. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT