proposition: Lemma filterlim_norm {K : AbsRing} {V : NormedModule K} : forall (x : V), filterlim norm (locally x) (locally (norm x)).
proof: Proof. intros x. apply (filterlim_filter_le_1 _ (locally_le_locally_norm x)). apply filterlim_locally => eps /=. exists eps ; move => /= y Hy. apply Rle_lt_trans with (2 := Hy). apply norm_triangle_inv. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub