proposition: Lemma atan_eq0 : forall x, atan x = 0 -> x = 0.
proof: Proof. intros x. generalize (atan_increasing 0 x) (atan_increasing x 0). rewrite atan_0. lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia