proposition: Lemma asin_ltpi2 x : -1 <= x < 1 -> asin x < pi/2.
proof: Proof. move=> /andP[x_geN1 x_lt1]; move: (x_lt1). have : asin x <= pi / 2 by rewrite asin_lepi2 // x_geN1 ltW. have : sin (asin x) = x by rewrite asinK// in_itv/= x_geN1 ltW. case: (ltrgtP _ ((pi / 2))) => // ->. by rewrite 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