proposition: Lemma derivable_scal : forall f a, derivable f -> derivable (mult_real_fct a f).
proof: Proof. intros f a Hf z ; apply derivable_pt_scal ; intuition. 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