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