Library Coq.Reals.Ranalysis3

Require Import Rbase.
Require Import Rfunctions.
Require Import Ranalysis1.
Require Import Ranalysis2.
Require Import Lra.
Local Open Scope R_scope.

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