proposition: Lemma is_derive1_acos (x : R) : -1 < x < 1 -> is_derive x 1 acos (- (Num.sqrt (1 - x ^+ 2))^-1).
proof: Proof. move=> /andP[x_gtN1 x_lt1]; rewrite -sin_acos ?ltW // -invrN. rewrite -{1}[x]acosK; last by have : -1 <= x <= 1 by rewrite ltW // ltW. have /near_in_itv aI : acos x \in `]0, pi[. suff : 0 < acos x < pi by []. by rewrite acos_gt0 ?ltW //= acos_ltpi // ltW ?andbT. apply: (@is_derive_inverse R cos). - near=> z; apply: cosK. suff /itvP zI : z \in `]0, pi[ by have : 0 <= z <= pi by rewrite ltW ?zI. by near: z. - by near=> z; apply: continuous_cos. - rewrite oppr_eq0 sin_acos ?ltW // sqrtr_eq0 // -ltNge subr_gt0. rewrite -real_normK ?qualifE/=; last by case: ltrgt0P. by rewrite exprn_cp1 // ltr_norml x_gtN1. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) reals ereal nsatz_realtype signed topology normedtype landau sequences derive realfun exp