proposition: Lemma derivable_pt_in_minus: forall (D : R -> Prop) (f g : R -> R) (x : R), derivable_pt_in D f x -> derivable_pt_in D g x -> derivable_pt_in D (f - g)%F x.
proof: Proof. intros D f g x [] []; eexists ; eapply derivable_pt_lim_in_minus ; eassumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics