proposition: Lemma is_derive1_asin (x : R) : -1 < x < 1 -> is_derive x 1 asin ((Num.sqrt (1 - x ^+ 2))^-1).
proof: Proof. move=> /andP[x_gtN1 x_lt1]; rewrite -cos_asin ?ltW //. rewrite -{1}[x]asinK; last by have : -1 <= x <= 1 by rewrite ltW // ltW. have /near_in_itv aI : asin x \in `](-(pi/2)), (pi/2)[. suff : -(pi/2) < asin x < pi/2 by []. by rewrite asin_gtNpi2 ?ltW ?andbT //= asin_ltpi2 // ltW. apply: (@is_derive_inverse R sin). - near=> z; apply: sinK. suff /itvP zI : z \in `](-(pi/2)), (pi/2)[. by have : - (pi / 2) <= z <= pi / 2 by rewrite ltW ?zI. by near: z. - by near=> z; exact: continuous_sin. - rewrite cos_asin ?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