proposition: Lemma derivable_in_div: forall (D : R -> Prop) f g, (forall x, D x -> g x <> 0) -> derivable_in D f -> derivable_in D g -> derivable_in D (f / g)%F.
proof: Proof. intros D f g Hneq Hf Hg x x_in ; apply derivable_pt_in_div ; [| apply Hneq | apply Hf | apply Hg] ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics