proposition: Lemma acos_gt0 x : -1 <= x < 1 -> 0 < acos x.
proof: Proof. move=> /andP[x_geN1 x_lt1]; move: (x_lt1). have : 0 <= acos x by rewrite acos_ge0 // x_geN1 ltW. have : cos (acos x) = x by rewrite acosK// in_itv/= x_geN1/= ltW. by case: ltrgt0P => // ->; rewrite cos0 => ->; 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