proposition: Lemma ArcTan_Tan_inv : Feq (olor [--] (Pi [/]TwoNZ) (Pi [/]TwoNZ)) (ArcTang[o]Tang) FId.
proof: Proof. set (HPi1 := pos_HalfPi) in *. set (HPi2 := neg_invHalfPi) in *. set (H := invHalfPi_less_HalfPi) in *. apply Feq_criterium with H ( [-C-][1]:PartIR) ZeroR. set (H0 := Derivative_Tan_2 H) in *. set (H2 := Derivative_ArcTan I) in *. Derivative_Help. apply eq_imp_Feq. apply included_FMult. apply included_FComp. Included. intros. split. repeat split. intros. astepl ([1][+]Tang x Hx[^]2). apply pos_ap_zero. astepl (ZeroR[+][0]); apply plus_resp_less_leEq. apply pos_one. apply sqr_nonneg. Included. Included. intros. astepr OneR. astepl (Part _ _ (ProjIR1 Hx) [*]Part _ _ (ProjIR2 Hx)). elim Hx; intros H3 H4. astepl (Part _ _ H3[*]Part _ _ H4). astepl (Part _ _ (ProjT2 H3) [*] (Part _ _ (ProjIR1 H4) [+]Part _ _ (ProjIR2 H4))). elim H3; intros x0 H5; elim H4; intros H6 H7. astepl (Part _ _ H5[*] (Part _ _ H6[+]Part _ _ H7)). astepl (Part _ _ H5[*] ([1][+]Tang x H7[^]2)). simpl in |- *; rational. apply Derivative_comp with realline I. apply maps_Tan. Deriv. Deriv. Deriv. split; auto. intros. astepr ZeroR. inversion_clear Hx. Opaque Tang. simpl in |- *. apply Integral_empty. algebra. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT