proposition: Lemma ps_atan0_0 : ps_atan 0 = 0.
proof: Proof. unfold ps_atan. destruct (in_int 0) as [h1 | h2]. { destruct (ps_atan_exists_1 0 h1) as [v P]. apply (UL_sequence _ _ _ P). apply (Un_cv_ext (fun n => 0)). { symmetry;apply sum_eq_R0. intros i _; unfold tg_alt, Ratan_seq; rewrite Nat.add_comm; simpl. unfold Rdiv; rewrite !Rmult_0_l, Rmult_0_r; reflexivity. } intros eps ep; exists 0%nat; intros n _; unfold Rdist. rewrite Rminus_0_r, Rabs_pos_eq; auto with real. } case h2; split; lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia