proposition: Lemma cosKN a : - pi <= a <= 0 -> acos (cos a) = - a.
proof: Proof. by move=> pia0; rewrite -(cosN a) cosK// in_itv/= lerNr oppr0 lerNl andbC. 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