proposition: Lemma continuity_pt_plus : forall f1 f2 (x0:R), continuity_pt f1 x0 -> continuity_pt f2 x0 -> continuity_pt (f1 + f2) x0.
proof: Proof. unfold continuity_pt, plus_fct; unfold continue_in; intros; apply limit_plus; assumption. Qed.
imports: Rbase Rfunctions Rlimit Rderiv