proposition: Theorem derivable_continuous : forall f, derivable f -> continuity f.
proof: Proof. unfold derivable, continuity in |- *; intros f X x. apply (derivable_continuous_pt f x (X x)). Qed.
imports: MyRIneq Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_usual Ranalysis_facts Ranalysis_MVT Canalysis_diff Cprop_base Cnorm Ctacfield Cmet Canalysis_def Cderiv