proposition: Lemma ps_atan_opp : forall x, ps_atan (-x) = -ps_atan x.
proof: Proof. intros x; unfold ps_atan. destruct (in_int (- x)) as [inside | outside]. { destruct (in_int x) as [ins' | outs']. { generalize (ps_atan_exists_1_opp x inside ins'). intros h; exact h. } destruct inside; case outs'; split; lra. } destruct (in_int x) as [ins' | outs']. { destruct outside; case ins'; split; lra. } apply atan_opp. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia