proposition: Lemma continuity_pt_opp : forall f (x0:R), continuity_pt f x0 -> continuity_pt (- f) x0.
proof: Proof. unfold continuity_pt, opp_fct; unfold continue_in; intros; apply limit_Ropp; assumption. Qed.
imports: Rbase Rfunctions Rlimit Rderiv