proposition: Lemma acos0 : acos (0 : R) = pi / 2%:R.
proof: Proof. have := @cosK (pi / 2%:R). rewrite cos_pihalf => -> //; rewrite in_itv//= divr_ge0 ?ler0n ?pi_ge0//=. by rewrite ler_pdivrMr ?ltr0n// ler_peMr ?pi_ge0// ler1n. 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