proposition: Lemma Tan_ArcTan_inv : Feq realline (Tang[o]ArcTang) FId.
proof: Proof. apply eq_imp_Feq. apply included_FComp. Included. intros; split. auto. split. auto. intros. apply ap_wdl with (Cos (ArcTan x)). Opaque ArcTang. 2: unfold ArcTan in |- *; simpl in |- *; algebra. elim ArcTan_range with x; intros. apply pos_ap_zero; apply Cos_pos; auto. Included. intros; inversion_clear Hx. astepr x; astepl (Part _ _ (ProjT2 Hx)); astepl (Part _ _ X0). cut (Dom Tang (ArcTan x)); intros. apply eq_transitive_unfolded with (Tan (ArcTan x) X1). unfold Tan, ArcTan in |- *; algebra. apply eq_symmetric_unfolded; apply Tan_ArcTan. apply dom_wd with (ArcTang x x0); auto. unfold ArcTan in |- *; algebra. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT