Library Stdlib.Reals.Rtrigo_fun

From Stdlib Require Import Rbase.
From Stdlib Require Import Rfunctions.
From Stdlib Require Import SeqSeries.
From Stdlib Require Import Arith.Factorial.
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.