proposition: Lemma derivable_pt_in_scal: forall D a f x, derivable_pt_in D f x -> derivable_pt_in D (mult_real_fct a f) x.
proof: Proof. intros D a f x [l Hl] ; eexists ; eapply derivable_pt_lim_in_scal ; eassumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics