proposition: Lemma derivable_in_continuity_in : forall f D, derivable_in D f -> continuity_in D f.
proof: Proof. intros f D Hf x Dx ; apply derivable_pt_in_continuity_pt_in. apply Hf ; assumption. assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics