proposition: Lemma filterlim_norm_zero {U} {K : AbsRing} {V : NormedModule K} {F : (U -> Prop) -> Prop} {FF : Filter F} (f : U -> V) : filterlim (fun x => norm (f x)) F (locally 0) -> filterlim f F (locally (zero (G := V))).
proof: Proof. intros Hf. apply filterlim_locally_ball_norm => eps. generalize (proj1 (filterlim_locally_ball_norm _ _) Hf eps) ; unfold ball_norm ; simpl. apply filter_imp => /= x. rewrite !minus_zero_r {1}/norm /= /abs /= Rabs_pos_eq //. by apply norm_ge_0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub