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