proposition: Lemma is_lim_mul_exp_m : is_lim (fun y => y * exp y) m_infty 0.
proof: Proof. evar_last. apply is_lim_ext_loc with (fun y => - / (exp (-y) / (- y))). exists 0 => y Hy. rewrite exp_Ropp. field. split. apply Rgt_not_eq, exp_pos. by apply Rlt_not_eq. apply is_lim_opp. apply is_lim_inv. apply (is_lim_comp (fun y => exp y / y)) with p_infty. by apply is_lim_div_exp_p. evar_last. apply is_lim_opp. apply is_lim_id. by []. by apply filter_forall. by []. simpl ; by rewrite Ropp_0. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis