proposition: Lemma Derivative_ArcCos : forall H, Derivative (olor [--][1] [1]) H ArcCos {--} (( [-C-][1]{-}FId{^}2) {!} [-C-] [--] ([1] [/]TwoNZ)).
proof: Proof. intros; unfold ArcCos in |- *. apply Derivative_wdr with ( [-C-][0]{-} ( [-C-][1]{-}FId{^}2) {!} [-C-] [--] ([1] [/]TwoNZ)). 2: Deriv. apply eq_imp_Feq. apply included_FMinus. Included. apply Continuous_imp_inc; apply ArcSin_def_lemma. apply included_FInv. apply Continuous_imp_inc; apply ArcSin_def_lemma. intros. astepl (Part _ _ (ProjIR1 Hx) [-]Part _ _ (ProjIR2 Hx)). astepl ([0][-]Part _ _ (ProjIR2 Hx)). astepl ( [--] (Part _ _ (ProjIR2 Hx))). Step_final ( [--] ((( [-C-][1]{-}FId{^}2) {!} [-C-] [--] ([1] [/]TwoNZ)) x Hx')). Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT