proposition: Lemma derivable_div : forall f1 f2:R -> R, derivable f1 -> derivable f2 -> (forall x:R, f2 x <> 0) -> derivable (f1 / f2).
proof: Proof. unfold derivable; intros f1 f2 X X0 H x. apply (derivable_pt_div _ _ _ (X x) (X0 x) (H x)). Qed.
imports: Rbase Rfunctions Ranalysis1 Ranalysis2 Lra