proposition: Lemma continuity_continuity_in: forall D f, continuity f -> continuity_in D f.
proof: Proof. intros D f f_cont x x_in ; apply continuity_pt_continuity_pt_in ; [apply f_cont |] ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Ranalysis_def_simpl Rfunction_facts MyRIneq MyR_dist Lra Tactics