Library Coq.Reals.Rtrigo_fun



Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Open Local Scope R_scope.

To define transcendental functions
and exponential function

Lemma Alembert_exp :
  Un_cv (fun n:nat => Rabs (/ INR (fact (S n)) * / / INR (fact n))) 0.