proposition: Lemma atan_bound : forall x, -PI/2 < atan x < PI/2.
proof: Proof. intros x; unfold atan; destruct (pre_atan x) as [v [int _]]; exact int. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia