proposition: Lemma atan_tan : forall x, - (PI / 2) < x < PI / 2 -> atan (tan x) = x.
proof: Proof. intros x xB. apply tan_inj. - now apply atan_bound. - lra. - now apply tan_atan. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia