Library Coq.Reals.Ranalysis3
Require
Import
Rbase
.
Require
Import
Rfunctions
.
Require
Import
Ranalysis1
.
Require
Import
Ranalysis2
.
Local
Open
Scope
R_scope
.
Division
Theorem
derivable_pt_lim_div
:
forall
(
f1
f2
:
R
->
R
) (
x
l1
l2
:
R
),
derivable_pt_lim
f1
x
l1
->
derivable_pt_lim
f2
x
l2
->
f2
x
<>
0 ->
derivable_pt_lim
(
f1
/
f2
)
x
(
(
l1
*
f2
x
-
l2
*
f1
x
)
/
Rsqr
(
f2
x
)).
Lemma
derivable_pt_div
:
forall
(
f1
f2
:
R
->
R
) (
x
:
R
),
derivable_pt
f1
x
->
derivable_pt
f2
x
->
f2
x
<>
0 ->
derivable_pt
(
f1
/
f2
)
x
.
Lemma
derivable_div
:
forall
f1
f2
:
R
->
R
,
derivable
f1
->
derivable
f2
-> (
forall
x
:
R
,
f2
x
<>
0) ->
derivable
(
f1
/
f2
).
Lemma
derive_pt_div
:
forall
(
f1
f2
:
R
->
R
) (
x
:
R
) (
pr1
:
derivable_pt
f1
x
)
(
pr2
:
derivable_pt
f2
x
) (
na
:
f2
x
<>
0),
derive_pt
(
f1
/
f2
)
x
(
derivable_pt_div
_
_
_
pr1
pr2
na
)
=
(
derive_pt
f1
x
pr1
*
f2
x
-
derive_pt
f2
x
pr2
*
f1
x
)
/
Rsqr
(
f2
x
).