proposition: Lemma cos_atan: forall x, cos (atan x) = 1 / sqrt(1 + x²).
proof: Proof. intros x. pose proof (atan_right_inv x) as Hatan. remember (atan(x)) as α. rewrite <- Hatan. apply cos_tan. apply cos_gt_0. 1,2: pose proof atan_bound x; lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia