proposition: Lemma continuity_in_opp : forall D f, continuity_in D f -> continuity_in D (- f)%F.
proof: Proof. intros D f Hf x x_in ; apply limit_Ropp ; eapply_assumption ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Ranalysis_def_simpl Rfunction_facts MyRIneq MyR_dist Lra Tactics