proposition: Lemma atan_1 : atan 1 = PI/4.
proof: Proof. assert (ut := PI_RGT_0). assert (-PI/2 < PI/4 < PI/2) by (rewrite Rdiv_opp_l; split; lra). assert (t := atan_bound 1). apply tan_inj; auto. rewrite tan_PI4, tan_atan; reflexivity. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia