proposition: Lemma asin_gtNpi2 x : -1 < x <= 1 -> - (pi / 2) < asin x.
proof: Proof. move=> /andP[x_gtN1 x_le1]; move: (x_gtN1). have : - (pi / 2) <= asin x by rewrite asin_geNpi2 // x_le1 ltW. have : sin (asin x) = x by rewrite asinK// in_itv/= x_le1 ltW. by case: (ltrgtP (asin x)) => //->; rewrite sinN sin_pihalf => <-; rewrite ltxx. 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