Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
C
coquelicot
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
1
Issues
1
List
Boards
Labels
Milestones
Merge Requests
1
Merge Requests
1
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Coquelicot
coquelicot
Commits
4a29fe56
Commit
4a29fe56
authored
Jul 29, 2013
by
Guillaume Melquiond
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Add copyright notice at the start of each file.
parent
74bb9190
Changes
23
Expand all
Hide whitespace changes
Inline
Sidebyside
Showing
23 changed files
with
621 additions
and
498 deletions
+621
498
COPYING
COPYING
+158
497
examples/BacS2013.v
examples/BacS2013.v
+21
0
examples/Bessel.v
examples/Bessel.v
+21
0
examples/DAlembert.v
examples/DAlembert.v
+21
0
theories/AutoDerive.v
theories/AutoDerive.v
+21
0
theories/Compactness.v
theories/Compactness.v
+21
0
theories/Continuity.v
theories/Continuity.v
+21
0
theories/Coquelicot.v
theories/Coquelicot.v
+22
1
theories/Derive.v
theories/Derive.v
+21
0
theories/Derive_2d.v
theories/Derive_2d.v
+21
0
theories/ElemFct.v
theories/ElemFct.v
+21
0
theories/Equiv.v
theories/Equiv.v
+21
0
theories/Limit.v
theories/Limit.v
+21
0
theories/Locally.v
theories/Locally.v
+21
0
theories/Lub.v
theories/Lub.v
+21
0
theories/Markov.v
theories/Markov.v
+21
0
theories/PSeries.v
theories/PSeries.v
+21
0
theories/RInt.v
theories/RInt.v
+21
0
theories/Rbar.v
theories/Rbar.v
+21
0
theories/Rcomplements.v
theories/Rcomplements.v
+21
0
theories/SF_seq.v
theories/SF_seq.v
+21
0
theories/Seq_fct.v
theories/Seq_fct.v
+21
0
theories/Series.v
theories/Series.v
+21
0
No files found.
COPYING
View file @
4a29fe56
This diff is collapsed.
Click to expand it.
examples/BacS2013.v
View file @
4a29fe56
(
**
This
file
is
part
of
the
Coquelicot
formalization
of
real
analysis
in
Coq
:
http
:
//coquelicot.saclay.inria.fr/
Copyright
(
C
)
2011

2013
Sylvie
Boldo
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Catherine
Lelay
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Guillaume
Melquiond
This
library
is
free
software
;
you
can
redistribute
it
and
/
or
modify
it
under
the
terms
of
the
GNU
Lesser
General
Public
License
as
published
by
the
Free
Software
Foundation
;
either
version
3
of
the
License
,
or
(
at
your
option
)
any
later
version
.
This
library
is
distributed
in
the
hope
that
it
will
be
useful
,
but
WITHOUT
ANY
WARRANTY
;
without
even
the
implied
warranty
of
MERCHANTABILITY
or
FITNESS
FOR
A
PARTICULAR
PURPOSE
.
See
the
COPYING
file
for
more
details
.
*
)
(
**
*
Bac
S
2013
*
)
(
**
https
:
//www.lri.fr/~lelay/Bac2013/Bac_S_2013_Metropole.pdf *)
...
...
examples/Bessel.v
View file @
4a29fe56
(
**
This
file
is
part
of
the
Coquelicot
formalization
of
real
analysis
in
Coq
:
http
:
//coquelicot.saclay.inria.fr/
Copyright
(
C
)
2011

2013
Sylvie
Boldo
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Catherine
Lelay
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Guillaume
Melquiond
This
library
is
free
software
;
you
can
redistribute
it
and
/
or
modify
it
under
the
terms
of
the
GNU
Lesser
General
Public
License
as
published
by
the
Free
Software
Foundation
;
either
version
3
of
the
License
,
or
(
at
your
option
)
any
later
version
.
This
library
is
distributed
in
the
hope
that
it
will
be
useful
,
but
WITHOUT
ANY
WARRANTY
;
without
even
the
implied
warranty
of
MERCHANTABILITY
or
FITNESS
FOR
A
PARTICULAR
PURPOSE
.
See
the
COPYING
file
for
more
details
.
*
)
Require
Import
Reals
ssreflect
.
Require
Import
Rcomplements
Rbar
.
Require
Import
Derive
Series
PSeries
Limit
.
...
...
examples/DAlembert.v
View file @
4a29fe56
(
**
This
file
is
part
of
the
Coquelicot
formalization
of
real
analysis
in
Coq
:
http
:
//coquelicot.saclay.inria.fr/
Copyright
(
C
)
2011

2013
Sylvie
Boldo
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Catherine
Lelay
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Guillaume
Melquiond
This
library
is
free
software
;
you
can
redistribute
it
and
/
or
modify
it
under
the
terms
of
the
GNU
Lesser
General
Public
License
as
published
by
the
Free
Software
Foundation
;
either
version
3
of
the
License
,
or
(
at
your
option
)
any
later
version
.
This
library
is
distributed
in
the
hope
that
it
will
be
useful
,
but
WITHOUT
ANY
WARRANTY
;
without
even
the
implied
warranty
of
MERCHANTABILITY
or
FITNESS
FOR
A
PARTICULAR
PURPOSE
.
See
the
COPYING
file
for
more
details
.
*
)
Require
Import
Reals
.
Require
Import
Rcomplements
Derive
RInt
Locally
Derive_2d
.
Require
Import
AutoDerive
.
...
...
theories/AutoDerive.v
View file @
4a29fe56
(
**
This
file
is
part
of
the
Coquelicot
formalization
of
real
analysis
in
Coq
:
http
:
//coquelicot.saclay.inria.fr/
Copyright
(
C
)
2011

2013
Sylvie
Boldo
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Catherine
Lelay
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Guillaume
Melquiond
This
library
is
free
software
;
you
can
redistribute
it
and
/
or
modify
it
under
the
terms
of
the
GNU
Lesser
General
Public
License
as
published
by
the
Free
Software
Foundation
;
either
version
3
of
the
License
,
or
(
at
your
option
)
any
later
version
.
This
library
is
distributed
in
the
hope
that
it
will
be
useful
,
but
WITHOUT
ANY
WARRANTY
;
without
even
the
implied
warranty
of
MERCHANTABILITY
or
FITNESS
FOR
A
PARTICULAR
PURPOSE
.
See
the
COPYING
file
for
more
details
.
*
)
Require
Import
Reals
.
Require
Import
Rcomplements
Locally
Derive
RInt
Derive_2d
Continuity
ElemFct
.
Require
Import
ssreflect
ssrbool
seq
Datatypes
.
...
...
theories/Compactness.v
View file @
4a29fe56
(
**
This
file
is
part
of
the
Coquelicot
formalization
of
real
analysis
in
Coq
:
http
:
//coquelicot.saclay.inria.fr/
Copyright
(
C
)
2011

2013
Sylvie
Boldo
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Catherine
Lelay
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Guillaume
Melquiond
This
library
is
free
software
;
you
can
redistribute
it
and
/
or
modify
it
under
the
terms
of
the
GNU
Lesser
General
Public
License
as
published
by
the
Free
Software
Foundation
;
either
version
3
of
the
License
,
or
(
at
your
option
)
any
later
version
.
This
library
is
distributed
in
the
hope
that
it
will
be
useful
,
but
WITHOUT
ANY
WARRANTY
;
without
even
the
implied
warranty
of
MERCHANTABILITY
or
FITNESS
FOR
A
PARTICULAR
PURPOSE
.
See
the
COPYING
file
for
more
details
.
*
)
Require
Import
Reals
.
Require
Import
ssreflect
.
Require
Import
List
.
...
...
theories/Continuity.v
View file @
4a29fe56
(
**
This
file
is
part
of
the
Coquelicot
formalization
of
real
analysis
in
Coq
:
http
:
//coquelicot.saclay.inria.fr/
Copyright
(
C
)
2011

2013
Sylvie
Boldo
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Catherine
Lelay
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Guillaume
Melquiond
This
library
is
free
software
;
you
can
redistribute
it
and
/
or
modify
it
under
the
terms
of
the
GNU
Lesser
General
Public
License
as
published
by
the
Free
Software
Foundation
;
either
version
3
of
the
License
,
or
(
at
your
option
)
any
later
version
.
This
library
is
distributed
in
the
hope
that
it
will
be
useful
,
but
WITHOUT
ANY
WARRANTY
;
without
even
the
implied
warranty
of
MERCHANTABILITY
or
FITNESS
FOR
A
PARTICULAR
PURPOSE
.
See
the
COPYING
file
for
more
details
.
*
)
Require
Import
Reals
.
Require
Import
ssreflect
.
Require
Import
Rcomplements
Rbar
Locally
.
...
...
theories/Coquelicot.v
View file @
4a29fe56
...
...
@@ 47,4 +47,25 @@ Naming conventions:
Require
Export
AutoDerive
Compactness
Continuity
Derive
.
Require
Export
Derive_2d
Equiv
ElemFct
Limit
.
Require
Export
Locally
Lub
Markov
PSeries
Rbar
Rcomplements
.
Require
Export
RInt
Seq_fct
Series
SF_seq
.
\ No newline at end of file
Require
Export
RInt
Seq_fct
Series
SF_seq
.
(
**
This
file
is
part
of
the
Coquelicot
formalization
of
real
analysis
in
Coq
:
http
:
//coquelicot.saclay.inria.fr/
Copyright
(
C
)
2011

2013
Sylvie
Boldo
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Catherine
Lelay
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Guillaume
Melquiond
This
library
is
free
software
;
you
can
redistribute
it
and
/
or
modify
it
under
the
terms
of
the
GNU
Lesser
General
Public
License
as
published
by
the
Free
Software
Foundation
;
either
version
3
of
the
License
,
or
(
at
your
option
)
any
later
version
.
This
library
is
distributed
in
the
hope
that
it
will
be
useful
,
but
WITHOUT
ANY
WARRANTY
;
without
even
the
implied
warranty
of
MERCHANTABILITY
or
FITNESS
FOR
A
PARTICULAR
PURPOSE
.
See
the
COPYING
file
for
more
details
.
*
)
theories/Derive.v
View file @
4a29fe56
(
**
This
file
is
part
of
the
Coquelicot
formalization
of
real
analysis
in
Coq
:
http
:
//coquelicot.saclay.inria.fr/
Copyright
(
C
)
2011

2013
Sylvie
Boldo
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Catherine
Lelay
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Guillaume
Melquiond
This
library
is
free
software
;
you
can
redistribute
it
and
/
or
modify
it
under
the
terms
of
the
GNU
Lesser
General
Public
License
as
published
by
the
Free
Software
Foundation
;
either
version
3
of
the
License
,
or
(
at
your
option
)
any
later
version
.
This
library
is
distributed
in
the
hope
that
it
will
be
useful
,
but
WITHOUT
ANY
WARRANTY
;
without
even
the
implied
warranty
of
MERCHANTABILITY
or
FITNESS
FOR
A
PARTICULAR
PURPOSE
.
See
the
COPYING
file
for
more
details
.
*
)
Require
Import
Reals
Rbar
.
Require
Import
ssreflect
.
Require
Import
Limit
.
...
...
theories/Derive_2d.v
View file @
4a29fe56
(
**
This
file
is
part
of
the
Coquelicot
formalization
of
real
analysis
in
Coq
:
http
:
//coquelicot.saclay.inria.fr/
Copyright
(
C
)
2011

2013
Sylvie
Boldo
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Catherine
Lelay
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Guillaume
Melquiond
This
library
is
free
software
;
you
can
redistribute
it
and
/
or
modify
it
under
the
terms
of
the
GNU
Lesser
General
Public
License
as
published
by
the
Free
Software
Foundation
;
either
version
3
of
the
License
,
or
(
at
your
option
)
any
later
version
.
This
library
is
distributed
in
the
hope
that
it
will
be
useful
,
but
WITHOUT
ANY
WARRANTY
;
without
even
the
implied
warranty
of
MERCHANTABILITY
or
FITNESS
FOR
A
PARTICULAR
PURPOSE
.
See
the
COPYING
file
for
more
details
.
*
)
Require
Import
Reals
.
Require
Import
ssreflect
.
Require
Import
Rcomplements
Locally
Continuity
Derive
.
...
...
theories/ElemFct.v
View file @
4a29fe56
(
**
This
file
is
part
of
the
Coquelicot
formalization
of
real
analysis
in
Coq
:
http
:
//coquelicot.saclay.inria.fr/
Copyright
(
C
)
2011

2013
Sylvie
Boldo
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Catherine
Lelay
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Guillaume
Melquiond
This
library
is
free
software
;
you
can
redistribute
it
and
/
or
modify
it
under
the
terms
of
the
GNU
Lesser
General
Public
License
as
published
by
the
Free
Software
Foundation
;
either
version
3
of
the
License
,
or
(
at
your
option
)
any
later
version
.
This
library
is
distributed
in
the
hope
that
it
will
be
useful
,
but
WITHOUT
ANY
WARRANTY
;
without
even
the
implied
warranty
of
MERCHANTABILITY
or
FITNESS
FOR
A
PARTICULAR
PURPOSE
.
See
the
COPYING
file
for
more
details
.
*
)
Require
Import
Reals
ssreflect
.
Require
Import
Rbar
Rcomplements
Continuity
Derive
Locally
.
...
...
theories/Equiv.v
View file @
4a29fe56
(
**
This
file
is
part
of
the
Coquelicot
formalization
of
real
analysis
in
Coq
:
http
:
//coquelicot.saclay.inria.fr/
Copyright
(
C
)
2011

2013
Sylvie
Boldo
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Catherine
Lelay
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Guillaume
Melquiond
This
library
is
free
software
;
you
can
redistribute
it
and
/
or
modify
it
under
the
terms
of
the
GNU
Lesser
General
Public
License
as
published
by
the
Free
Software
Foundation
;
either
version
3
of
the
License
,
or
(
at
your
option
)
any
later
version
.
This
library
is
distributed
in
the
hope
that
it
will
be
useful
,
but
WITHOUT
ANY
WARRANTY
;
without
even
the
implied
warranty
of
MERCHANTABILITY
or
FITNESS
FOR
A
PARTICULAR
PURPOSE
.
See
the
COPYING
file
for
more
details
.
*
)
Require
Import
Reals
ssreflect
.
Require
Import
Rbar
Rcomplements
Locally
.
...
...
theories/Limit.v
View file @
4a29fe56
(
**
This
file
is
part
of
the
Coquelicot
formalization
of
real
analysis
in
Coq
:
http
:
//coquelicot.saclay.inria.fr/
Copyright
(
C
)
2011

2013
Sylvie
Boldo
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Catherine
Lelay
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Guillaume
Melquiond
This
library
is
free
software
;
you
can
redistribute
it
and
/
or
modify
it
under
the
terms
of
the
GNU
Lesser
General
Public
License
as
published
by
the
Free
Software
Foundation
;
either
version
3
of
the
License
,
or
(
at
your
option
)
any
later
version
.
This
library
is
distributed
in
the
hope
that
it
will
be
useful
,
but
WITHOUT
ANY
WARRANTY
;
without
even
the
implied
warranty
of
MERCHANTABILITY
or
FITNESS
FOR
A
PARTICULAR
PURPOSE
.
See
the
COPYING
file
for
more
details
.
*
)
Require
Import
Reals
ssreflect
.
Require
Import
Rcomplements
.
Require
Import
Rbar
Lub
Markov
Locally
.
...
...
theories/Locally.v
View file @
4a29fe56
(
**
This
file
is
part
of
the
Coquelicot
formalization
of
real
analysis
in
Coq
:
http
:
//coquelicot.saclay.inria.fr/
Copyright
(
C
)
2011

2013
Sylvie
Boldo
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Catherine
Lelay
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Guillaume
Melquiond
This
library
is
free
software
;
you
can
redistribute
it
and
/
or
modify
it
under
the
terms
of
the
GNU
Lesser
General
Public
License
as
published
by
the
Free
Software
Foundation
;
either
version
3
of
the
License
,
or
(
at
your
option
)
any
later
version
.
This
library
is
distributed
in
the
hope
that
it
will
be
useful
,
but
WITHOUT
ANY
WARRANTY
;
without
even
the
implied
warranty
of
MERCHANTABILITY
or
FITNESS
FOR
A
PARTICULAR
PURPOSE
.
See
the
COPYING
file
for
more
details
.
*
)
Require
Import
Reals
Rbar
.
Require
Import
ssreflect
.
Require
Import
Rcomplements
.
...
...
theories/Lub.v
View file @
4a29fe56
(
**
This
file
is
part
of
the
Coquelicot
formalization
of
real
analysis
in
Coq
:
http
:
//coquelicot.saclay.inria.fr/
Copyright
(
C
)
2011

2013
Sylvie
Boldo
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Catherine
Lelay
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Guillaume
Melquiond
This
library
is
free
software
;
you
can
redistribute
it
and
/
or
modify
it
under
the
terms
of
the
GNU
Lesser
General
Public
License
as
published
by
the
Free
Software
Foundation
;
either
version
3
of
the
License
,
or
(
at
your
option
)
any
later
version
.
This
library
is
distributed
in
the
hope
that
it
will
be
useful
,
but
WITHOUT
ANY
WARRANTY
;
without
even
the
implied
warranty
of
MERCHANTABILITY
or
FITNESS
FOR
A
PARTICULAR
PURPOSE
.
See
the
COPYING
file
for
more
details
.
*
)
Require
Import
Reals
ssreflect
.
Require
Import
Rbar
Rcomplements
Markov
.
...
...
theories/Markov.v
View file @
4a29fe56
(
**
This
file
is
part
of
the
Coquelicot
formalization
of
real
analysis
in
Coq
:
http
:
//coquelicot.saclay.inria.fr/
Copyright
(
C
)
2011

2013
Sylvie
Boldo
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Catherine
Lelay
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Guillaume
Melquiond
This
library
is
free
software
;
you
can
redistribute
it
and
/
or
modify
it
under
the
terms
of
the
GNU
Lesser
General
Public
License
as
published
by
the
Free
Software
Foundation
;
either
version
3
of
the
License
,
or
(
at
your
option
)
any
later
version
.
This
library
is
distributed
in
the
hope
that
it
will
be
useful
,
but
WITHOUT
ANY
WARRANTY
;
without
even
the
implied
warranty
of
MERCHANTABILITY
or
FITNESS
FOR
A
PARTICULAR
PURPOSE
.
See
the
COPYING
file
for
more
details
.
*
)
Require
Import
RIneq
Rcomplements
.
Open
Scope
R_scope
.
...
...
theories/PSeries.v
View file @
4a29fe56
(
**
This
file
is
part
of
the
Coquelicot
formalization
of
real
analysis
in
Coq
:
http
:
//coquelicot.saclay.inria.fr/
Copyright
(
C
)
2011

2013
Sylvie
Boldo
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Catherine
Lelay
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Guillaume
Melquiond
This
library
is
free
software
;
you
can
redistribute
it
and
/
or
modify
it
under
the
terms
of
the
GNU
Lesser
General
Public
License
as
published
by
the
Free
Software
Foundation
;
either
version
3
of
the
License
,
or
(
at
your
option
)
any
later
version
.
This
library
is
distributed
in
the
hope
that
it
will
be
useful
,
but
WITHOUT
ANY
WARRANTY
;
without
even
the
implied
warranty
of
MERCHANTABILITY
or
FITNESS
FOR
A
PARTICULAR
PURPOSE
.
See
the
COPYING
file
for
more
details
.
*
)
Require
Import
Reals
Even
Div2
ssreflect
.
Require
Import
Rcomplements
Rbar
Limit
Lub
.
Require
Import
Continuity
Derive
Derive_2d
RInt
Locally
Seq_fct
Series
.
...
...
theories/RInt.v
View file @
4a29fe56
(
**
This
file
is
part
of
the
Coquelicot
formalization
of
real
analysis
in
Coq
:
http
:
//coquelicot.saclay.inria.fr/
Copyright
(
C
)
2011

2013
Sylvie
Boldo
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Catherine
Lelay
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Guillaume
Melquiond
This
library
is
free
software
;
you
can
redistribute
it
and
/
or
modify
it
under
the
terms
of
the
GNU
Lesser
General
Public
License
as
published
by
the
Free
Software
Foundation
;
either
version
3
of
the
License
,
or
(
at
your
option
)
any
later
version
.
This
library
is
distributed
in
the
hope
that
it
will
be
useful
,
but
WITHOUT
ANY
WARRANTY
;
without
even
the
implied
warranty
of
MERCHANTABILITY
or
FITNESS
FOR
A
PARTICULAR
PURPOSE
.
See
the
COPYING
file
for
more
details
.
*
)
Require
Import
Reals
Div2
ConstructiveEpsilon
.
Require
Import
ssreflect
ssrbool
eqtype
seq
.
Require
Import
Markov
Rcomplements
Rbar
Lub
Limit
Derive
SF_seq
.
...
...
theories/Rbar.v
View file @
4a29fe56
(
**
This
file
is
part
of
the
Coquelicot
formalization
of
real
analysis
in
Coq
:
http
:
//coquelicot.saclay.inria.fr/
Copyright
(
C
)
2011

2013
Sylvie
Boldo
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Catherine
Lelay
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Guillaume
Melquiond
This
library
is
free
software
;
you
can
redistribute
it
and
/
or
modify
it
under
the
terms
of
the
GNU
Lesser
General
Public
License
as
published
by
the
Free
Software
Foundation
;
either
version
3
of
the
License
,
or
(
at
your
option
)
any
later
version
.
This
library
is
distributed
in
the
hope
that
it
will
be
useful
,
but
WITHOUT
ANY
WARRANTY
;
without
even
the
implied
warranty
of
MERCHANTABILITY
or
FITNESS
FOR
A
PARTICULAR
PURPOSE
.
See
the
COPYING
file
for
more
details
.
*
)
Require
Import
Reals
.
Require
Import
ssreflect
.
Require
Import
Rcomplements
.
...
...
theories/Rcomplements.v
View file @
4a29fe56
(
**
This
file
is
part
of
the
Coquelicot
formalization
of
real
analysis
in
Coq
:
http
:
//coquelicot.saclay.inria.fr/
Copyright
(
C
)
2011

2013
Sylvie
Boldo
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Catherine
Lelay
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Guillaume
Melquiond
This
library
is
free
software
;
you
can
redistribute
it
and
/
or
modify
it
under
the
terms
of
the
GNU
Lesser
General
Public
License
as
published
by
the
Free
Software
Foundation
;
either
version
3
of
the
License
,
or
(
at
your
option
)
any
later
version
.
This
library
is
distributed
in
the
hope
that
it
will
be
useful
,
but
WITHOUT
ANY
WARRANTY
;
without
even
the
implied
warranty
of
MERCHANTABILITY
or
FITNESS
FOR
A
PARTICULAR
PURPOSE
.
See
the
COPYING
file
for
more
details
.
*
)
Require
Import
Reals
ssreflect
.
Require
Import
Even
Div2
.
Require
Import
seq
ssrbool
.
...
...
theories/SF_seq.v
View file @
4a29fe56
(
**
This
file
is
part
of
the
Coquelicot
formalization
of
real
analysis
in
Coq
:
http
:
//coquelicot.saclay.inria.fr/
Copyright
(
C
)
2011

2013
Sylvie
Boldo
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Catherine
Lelay
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Guillaume
Melquiond
This
library
is
free
software
;
you
can
redistribute
it
and
/
or
modify
it
under
the
terms
of
the
GNU
Lesser
General
Public
License
as
published
by
the
Free
Software
Foundation
;
either
version
3
of
the
License
,
or
(
at
your
option
)
any
later
version
.
This
library
is
distributed
in
the
hope
that
it
will
be
useful
,
but
WITHOUT
ANY
WARRANTY
;
without
even
the
implied
warranty
of
MERCHANTABILITY
or
FITNESS
FOR
A
PARTICULAR
PURPOSE
.
See
the
COPYING
file
for
more
details
.
*
)
Require
Import
Reals
.
Require
Import
Rcomplements
Rbar
Lub
.
Require
Import
ssreflect
seq
ssrbool
.
...
...
theories/Seq_fct.v
View file @
4a29fe56
(
**
This
file
is
part
of
the
Coquelicot
formalization
of
real
analysis
in
Coq
:
http
:
//coquelicot.saclay.inria.fr/
Copyright
(
C
)
2011

2013
Sylvie
Boldo
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Catherine
Lelay
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Guillaume
Melquiond
This
library
is
free
software
;
you
can
redistribute
it
and
/
or
modify
it
under
the
terms
of
the
GNU
Lesser
General
Public
License
as
published
by
the
Free
Software
Foundation
;
either
version
3
of
the
License
,
or
(
at
your
option
)
any
later
version
.
This
library
is
distributed
in
the
hope
that
it
will
be
useful
,
but
WITHOUT
ANY
WARRANTY
;
without
even
the
implied
warranty
of
MERCHANTABILITY
or
FITNESS
FOR
A
PARTICULAR
PURPOSE
.
See
the
COPYING
file
for
more
details
.
*
)
Require
Import
Reals
ssreflect
Rbar
.
Require
Import
Rcomplements
Locally
.
Require
Import
Limit
Continuity
Derive
Series
.
...
...
theories/Series.v
View file @
4a29fe56
(
**
This
file
is
part
of
the
Coquelicot
formalization
of
real
analysis
in
Coq
:
http
:
//coquelicot.saclay.inria.fr/
Copyright
(
C
)
2011

2013
Sylvie
Boldo
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Catherine
Lelay
#
<
br
/>
#
Copyright
(
C
)
2011

2013
Guillaume
Melquiond
This
library
is
free
software
;
you
can
redistribute
it
and
/
or
modify
it
under
the
terms
of
the
GNU
Lesser
General
Public
License
as
published
by
the
Free
Software
Foundation
;
either
version
3
of
the
License
,
or
(
at
your
option
)
any
later
version
.
This
library
is
distributed
in
the
hope
that
it
will
be
useful
,
but
WITHOUT
ANY
WARRANTY
;
without
even
the
implied
warranty
of
MERCHANTABILITY
or
FITNESS
FOR
A
PARTICULAR
PURPOSE
.
See
the
COPYING
file
for
more
details
.
*
)
Require
Import
Reals
ssreflect
.
Require
Import
Rcomplements
.
Require
Import
Limit
Rbar
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment