proposition: Lemma atan_0 : atan 0 = 0.
proof: Proof. apply tan_inj; try (apply atan_bound). { assert (t := PI_RGT_0); rewrite Rdiv_opp_l; split; lra. } rewrite tan_atan, tan_0. reflexivity. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia