Home
About Coq
Get Coq
Documentation
Community
The Coq Proof Assistant
Library Coq.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.
Navigation
Standard Library
Table of contents
Index