proposition: Lemma derivable_pt_lim_in_scal: forall D a f x l, derivable_pt_lim_in D f x l -> derivable_pt_lim_in D (mult_real_fct a f) x (a * l).
proof: Proof. intros D a f x l Hf ; destruct (Req_dec a 0). subst ; rewrite Rmult_0_l ; eapply derivable_pt_lim_in_ext. symmetry ; eapply mult_real_fct_0. apply derivable_pt_lim_in_const. intros eps eps_pos ; pose (eps' := eps / Rabs a). assert (eps'_pos: 0 < eps'). apply Rlt_mult_inv_pos ; [| apply Rabs_pos_lt] ; assumption. destruct (Hf _ eps'_pos) as [alpha [alpha_pos Halpha]]. exists alpha ; split. assumption. intros y [[y_in y_neq] y_bd] ; rewrite growth_rate_mult_real_fct_compat, R_dist_scal_compat. apply Rlt_le_trans with (Rabs a * eps'). apply Rmult_lt_compat_l ; [apply Rabs_pos_lt | apply Halpha ; repeat split] ; assumption. right ; unfold eps' ; field ; apply Rabs_no_R0 ; assumption. split ; [exact I | assumption]. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics