proposition: Lemma filterlim_ext : forall {T U F G} {FF : Filter F} (f g : T -> U), (forall x, f x = g x) -> filterlim f F G -> filterlim g F G.
proof: Proof. intros T U F G FF f g Efg. apply filterlim_ext_loc. now apply filter_forall. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub