proposition: Lemma filterlim_ext_loc : forall {T U F G} {FF : Filter F} (f g : T -> U), F (fun x => f x = g x) -> filterlim f F G -> filterlim g F G.
proof: Proof. intros T U F G FF f g Efg Lf P GP. specialize (Lf P GP). generalize (filter_and _ (fun x : T => P (f x)) Efg Lf). unfold filtermap. apply filter_imp. now intros x [-> H]. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub