proposition: Lemma ex_lim_seq_abs (u : nat -> R) : ex_lim_seq u -> ex_lim_seq (fun n => Rabs (u n)).
proof: Proof. move => [l Hu]. exists (Rbar_abs l) ; by apply is_lim_seq_abs. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy