proposition: Lemma derivable_pt_lim_atan : forall x, derivable_pt_lim atan x (/ (1 + x^2)).
proof: Proof. intros x. apply derive_pt_eq_1 with (derivable_pt_atan x). replace (x ^ 2) with (x * x) by ring. rewrite <- (Rmult_1_l (Rinv _)). apply derive_pt_atan. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia