proposition: Lemma sinK : {in `[(- (pi / 2)), pi / 2], cancel sin asin}.
proof: Proof. move=> x; rewrite !in_itv/= => xB ; apply: sin_inj => //; last first. by rewrite asinK// in_itv/= sin_geN1 sin_le1. by rewrite in_itv/= asin_geNpi2/= ?asin_lepi2 ?sin_geN1 ?sin_le1. 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