proposition: Lemma derivable_pt_ps_atan : forall x, -1 < x < 1 -> derivable_pt ps_atan x.
proof: Proof. intros x x_encad. exists (/(1 + x^2)) ; apply derivable_pt_lim_ps_atan; assumption. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia