proposition: Lemma filterlimi_const {T} {U : UniformSpace} {F : (T -> Prop) -> Prop} {FF : Filter F} : forall (f : T -> U -> Prop) (a : U), (forall x, f x a) -> filterlimi f F (locally a).
proof: Proof. intros f a Hf. apply filterlimi_const_loc. exact: filter_forall. Qed.
imports: Coq(Reals List Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool) Stdlib Coquelicot Xreal Interval Taylor_model Interval_compl