proposition: Lemma derivable_in_opp: forall (D : R -> Prop) f, derivable_in D f -> derivable_in D (- f)%F.
proof: Proof. intros D f Hf x x_in ; eapply derivable_pt_in_opp, Hf ; eassumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics