proposition: Lemma is_lim_seq_abs (u : nat -> R) (l : Rbar) : is_lim_seq u l -> is_lim_seq (fun n => Rabs (u n)) (Rbar_abs l).
proof: Proof. intros Hu. apply filterlim_comp with (1 := Hu). apply filterlim_Rabs. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy