proposition: Lemma limit_scal: forall a f D x l, limit1_in f D l x -> limit1_in (mult_real_fct a f) D (a * l) x.
proof: Proof. intros a f D x l Hf eps eps_pos ; destruct (Req_dec a 0). exists 1 ; split ; [lra | intros y [y_in y_bd]] ; unfold mult_real_fct ; simpl ; subst ; rewrite R_dist_scal_compat, Rabs_R0, Rmult_0_l ; assumption. 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 Hy ; unfold mult_real_fct ; simpl. rewrite R_dist_scal_compat ; apply Rlt_le_trans with (Rabs a * eps'). apply Rmult_lt_compat_l ; [apply Rabs_pos_lt ; assumption |] ; apply Halpha ; assumption. right ; unfold eps' ; field ; apply Rabs_no_R0 ; assumption. Qed.
imports: Rbase Ranalysis Lia Lra Rfunctions Rfunction_facts Rextensionality Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rfunction_classes_def MyR_dist Reals.Tactics