proposition: Lemma ArcTan_Tan : forall x, [--] (Pi [/]TwoNZ) [<] x -> x [<] Pi [/]TwoNZ -> forall H, ArcTan (Tan x H) [=] x.
proof: Proof. intros. unfold Tan, ArcTan in |- *. astepr (FId x I). cut (Dom (ArcTang[o]Tang) x). intro H2. apply eq_transitive_unfolded with ((ArcTang[o]Tang) x H2). simpl in |- *; algebra. apply Feq_imp_eq with (olor [--] (Pi [/]TwoNZ) (Pi [/]TwoNZ)). apply ArcTan_Tan_inv. split; auto. exists H; apply I. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT