proposition: Lemma is_derive_atan x : is_derive atan x (/ (1 + x²)).
proof: Proof. rewrite Rsqr_pow2. apply is_derive_Reals, derivable_pt_lim_atan. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis