proposition: Lemma is_lim_seq_abs_0 (u : nat -> R) : is_lim_seq u 0 <-> is_lim_seq (fun n => Rabs (u n)) 0.
proof: Proof. split => Hu. rewrite -Rabs_R0. by apply (is_lim_seq_abs _ 0). apply is_lim_seq_spec in Hu. apply is_lim_seq_spec. move => eps. case: (Hu eps) => {Hu} N Hu. exists N => n Hn. move: (Hu n Hn) ; by rewrite ?Rminus_0_r Rabs_Rabsolu. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy