proposition: Lemma filterlim_Rabs : forall l : Rbar, filterlim Rabs (Rbar_locally l) (Rbar_locally (Rbar_abs l)).
proof: Proof. case => [l| |] /=. apply @filterlim_norm. intros P [N HP]. exists N => x Hx. apply HP. apply Rlt_le_trans with (1 := Hx). apply Rle_abs. intros P [N HP]. exists (-N) => x Hx. apply HP. apply Rlt_le_trans with (2 := Rabs_maj2 _), Ropp_lt_cancel. by rewrite Ropp_involutive. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy