proposition: Lemma atanN x : atan (- x) = - atan x.
proof: Proof. apply: tan_inj; first by rewrite in_itv/= atan_ltpi2 atan_gtNpi2. - by rewrite in_itv/= ltrNl opprK ltrNl andbC atan_ltpi2 atan_gtNpi2. - by rewrite tanN !atanK. 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