proposition: Theorem derivable_differentiable_pt : forall f x, derivable_pt f x -> forall v, differentiable_pt f x v.
proof: Proof. intros f x [l Hl] v ; exists l ; apply derivable_differentiable_pt_abs ; assumption. 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