proposition: Lemma at_point_filter_prod : forall {T F} { FF : Filter F} a (P : R -> T -> Prop), filter_prod (at_point a) F (fun ab : R * T => P ab.1 ab.2) -> F (P a).
proof: Proof. move => T F FF a P [Q R inQ inR H]. apply: filter_imp inR. move => x; exact: H. Qed.
imports: Coq(Reals List Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool) Stdlib Coquelicot Xreal Interval Taylor_model Interval_compl