proposition: Lemma filterlim_const : forall {T} {U : UniformSpace} {F : (T -> Prop) -> Prop} {FF : Filter F}, forall a : U, filterlim (fun _ => a) F (locally a).
proof: Proof. intros T U F FF a P [eps HP]. unfold filtermap. apply filter_forall. intros _. apply HP. apply ball_center. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub