proposition: Lemma continuous_acos x : -1 < x < 1 -> {for x, continuous acos}.
proof: Proof. move=> /andP[x_gtN1 x_lt1]; rewrite -[x]acosK; 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_cos. have /near_in_itv aI : acos x \in `]0, pi[. suff : 0 < acos x < pi by []. by rewrite acos_gt0 ?ltW //= acos_ltpi // ltW ?andbT. near=> z; apply: cosK. suff /itvP zI : z \in `]0, pi[ by have : 0 <= z <= pi 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