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