proposition: Lemma ArcTan_range : [--] (Pi [/]TwoNZ) [<] ArcTan x and ArcTan x [<] Pi [/]TwoNZ.
proof: Proof. intros. Transparent ArcTang. elim ArcTan_range_lemma; intros y H H0. elim H; intros. cut (Dom Tang y). intro H1. assert (H2 : Tan y H1 [=] x). unfold Tan in |- *; algebra. split. apply less_wdr with y; auto. apply eq_symmetric_unfolded; eapply eq_transitive_unfolded. 2: apply ArcTan_Tan with (H := H1); auto. unfold ArcTan in |- *; algebra. apply less_wdl with y; auto. apply eq_symmetric_unfolded; eapply eq_transitive_unfolded. 2: apply ArcTan_Tan with (H := H1); auto. unfold ArcTan in |- *; algebra. repeat split. intro; apply Greater_imp_ap. apply less_wdr with (Cos y); [ apply Cos_pos; auto | simpl in |- *; algebra ]. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT