Library Stdlib.Reals.Rtrigo_fun


Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Local Open 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.