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