proposition: Lemma derive_pt_minus : forall f g x prf prg pr, derive_pt (f - g)%F x pr = derive_pt f x prf - derive_pt g x prg.
proof: Proof. intros f g x prf prg pr ; erewrite pr_nu_var with (pr2 := derivable_pt_minus _ _ x prf prg) ; [apply derive_pt_minus | reflexivity]. Qed.
imports: Rbase Rpower Ranalysis Lra Rfunctions Rfunction_def Rextensionality MyRIneq MyR_dist Rtopology Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity