proposition: Lemma continuous_atan x : {for x, continuous atan}.
proof: Proof. rewrite -[x]atanK. have /near_in_itv aI : atan x \in `](-(pi / 2)), (pi / 2)[. suff : - (pi / 2) < atan x < pi / 2 by []. by rewrite atan_gtNpi2 atan_ltpi2. apply: nbhs_singleton (near_can_continuous _ _); last first. by near=> z; apply/continuous_tan/lt0r_neq0/cos_gt0_pihalf; near: z. by near=> z; apply: tanK; near: z. Unshelve. all: by end_near. 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