proposition: Lemma maps_Sin : maps_compacts_into (olor [--] (Pi [/]TwoNZ) (Pi [/]TwoNZ)) (olor [--][1] [1]) Sine.
proof: Proof. intros a b Hab H. set (min := Min (Sin a) [--] ([1] [/]TwoNZ)) in *. set (max := Max (Sin b) ([1] [/]TwoNZ)) in *. cut (min [<] max). intro H0. exists min; exists max; exists H0. elim (H _ (compact_inc_lft _ _ Hab)); intros Ha1 Ha2. elim (H _ (compact_inc_rht _ _ Hab)); intros Hb1 Hb2. split. intros x H1. unfold Nat.min, Nat.max in H1; inversion_clear H1; split. apply less_leEq_trans with min. unfold Nat.min in |- *; apply less_Min. apply inv_cancel_less; astepr OneR. eapply leEq_less_trans. apply inv_leEq_AbsIR. apply Abs_Sin_less_One; auto. apply inv_resp_less; apply (half_lt1 IR). auto. eapply leEq_less_trans. apply H3. apply Max_less. eapply leEq_less_trans. apply leEq_AbsIR. apply Abs_Sin_less_One; auto. apply (half_lt1 IR). intros x Hx H1. apply compact_wd with (Sin x). 2: simpl in |- *; algebra. unfold Nat.min, Nat.max in |- *; inversion_clear H1. split. eapply leEq_transitive; [ apply Min_leEq_lft | apply Sin_resp_leEq; auto ]. apply less_leEq; auto. apply less_leEq; apply leEq_less_trans with b; auto. eapply leEq_transitive. 2: apply lft_leEq_Max. apply Sin_resp_leEq; auto. apply leEq_transitive with a; auto; apply less_leEq; auto. apply less_leEq; auto. unfold Nat.min, Nat.max in |- *; apply less_transitive_unfolded with ZeroR. eapply leEq_less_trans. apply Min_leEq_rht. astepr ( [--][0]:IR); apply inv_resp_less; apply (pos_half IR). eapply less_leEq_trans; [ apply (pos_half IR) | apply rht_leEq_Max ]. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT