proposition: Lemma acos_def x : -1 <= x <= 1 -> 0 <= acos x <= pi /\ cos (acos x) = x.
proof: Proof. move=> xB; rewrite /acos; case: xgetP => //= He. pose f y := cos y - x. have /(IVT (@pi_ge0 _))[] // : minr (f 0) (f pi) <= 0 <= maxr (f 0) (f pi). rewrite /f cos0 cospi /minr /maxr ltrD2r -subr_lt0 opprK (_ : 1 + 1 = 2)//. by rewrite ltrn0 subr_le0 subr_ge0. - move=> y y0pi. by apply: continuousB; apply/continuous_in_subspaceT => ? ?; [exact: continuous_cos|exact: cst_continuous]. - rewrite /f => x1 /itvP x1I /eqP; rewrite subr_eq0 => /eqP cosx1E. 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