proposition: Lemma Derivative_ArcTan : forall H, Derivative realline H ArcTang {1/} ( [-C-][1]{+}FId{^}2).
proof: Proof. intros; unfold ArcTang in |- *; apply FTC1. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT