proposition: Lemma acosN a : -1 <= a <= 1 -> acos (- a) = pi - acos a.
proof: Proof. move=> a1; have ? : -1 <= - a <= 1 by rewrite lerNl opprK lerNl andbC. apply: cos_inj; first by rewrite in_itv/= acos_ge0//= acos_lepi. - by rewrite in_itv/= subr_ge0 acos_lepi//= lerBlDl lerDr acos_ge0. - by rewrite addrC cosDpi cosN !acosK. 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