Library Coq.Reals.Ranalysis3
Require
Import
Rbase
.
Require
Import
Rfunctions
.
Require
Import
Ranalysis1
.
Require
Import
Ranalysis2
.
Open
Local
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
).