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