proposition: Lemma tan_atan : forall x, tan (atan x) = x.
proof: Proof. intros x; unfold atan; destruct (pre_atan x) as [v [_ q]]; exact q. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia