# 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).