fact: Definition extend_continuously (f : R -> R) (a b : R) (x : R) : R.
imports: Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_usual Ranalysis_facts Rbase MyRIneq MyR_dist Rfunctions Lra