proposition: Lemma asin_def x : -1 <= x <= 1 -> -(pi / 2) <= asin x <= pi / 2 /\ sin (asin x) = x.
proof: Proof. move=> xB; rewrite /asin; case: xgetP => //= He. pose f y := sin y - x. have /IVT[] // : minr (f (-(pi/2))) (f (pi/2)) <= 0 <= maxr (f (-(pi/2))) (f (pi/2)). rewrite /f sinN sin_pihalf /minr /maxr ltrD2r -subr_gt0 opprK. by rewrite (_ : 1 + 1 = 2)// ltr0n/= subr_le0 subr_ge0. - by rewrite -subr_ge0 opprK -splitr pi_ge0. - by move=> *; apply: continuousB; apply/continuous_in_subspaceT => ? ?; [exact: continuous_sin| exact: cst_continuous]. - rewrite /f => x1 /itvP x1I /eqP; rewrite subr_eq0 => /eqP sinx1E. by case: (He x1); rewrite !x1I. 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