proposition: Lemma derivable_in_scal: forall D a f, derivable_in D f -> derivable_in D (mult_real_fct a f).
proof: Proof. intros D a f Hf x x_in ; specialize (Hf x x_in); apply derivable_pt_in_scal ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics