proposition: Lemma is_lim_Rabs (f : R -> R) (x l : Rbar) : is_lim f x l -> is_lim (fun x => Rabs (f x)) x (Rbar_abs l).
proof: Proof. destruct l as [l| | ] ; simpl ; intros ; first last. eapply is_lim_comp. 2: by apply H. by apply filterlim_Rabs. destruct x ; by exists (mkposreal _ Rlt_0_1). eapply is_lim_comp. 2: by apply H. by apply filterlim_Rabs. destruct x ; by exists (mkposreal _ Rlt_0_1). apply is_lim_comp_continuous => //. by apply continuous_Rabs. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis