proposition: Lemma acos_ltpi x : -1 < x <= 1 -> acos x < pi.
proof: Proof. move=> /andP[x_gtN1 x_le1]; move: (x_gtN1). have : acos x <= pi by rewrite acos_lepi // x_le1 ltW. have : cos (acos x) = x by rewrite acosK// in_itv/= x_le1 ltW. by case: (ltrgtP (acos x) pi) => // ->; rewrite cospi => ->; 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