proposition: Lemma derivable_pt_lim_in_div: forall (D : R -> Prop) f g x l1 l2, D x -> g x <> 0 -> derivable_pt_lim_in D f x l1 -> derivable_pt_lim_in D g x l2 -> derivable_pt_lim_in D (f / g)%F x ((l1 * g x - f x * l2) / g x ^ 2).
proof: Proof. intros D f g x l1 l2 Dx Hneq Hf Hg ; apply derivable_pt_lim_in_ext with (f * / g)%F. intro ; reflexivity. replace ((l1 * g x - f x * l2) / g x ^ 2) with ((l1 * (/ g)%F x) + f x * (- l2 / g x ^ 2)). eapply derivable_pt_lim_in_mult ; try eassumption. eapply derivable_pt_lim_in_inv ; try eassumption. unfold inv_fct ; field ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics