proposition: Lemma continuous_asin x : -1 < x < 1 -> {for x, continuous asin}.
proof: Proof. move=> /andP[x_gtN1 x_lt1]; rewrite -[x]asinK; first last. by have : -1 <= x <= 1 by rewrite !ltW //; case/andP: xB. apply: nbhs_singleton (near_can_continuous _ _); last first. by near=> z; apply: continuous_sin. 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. 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. 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